Who Cites type tag?
type_tag	Def type_tag(x;'a) == x
	Thm* 'a:Type, x:'a. type_tag(x;'a)  'a

Syntax:

type_tag(x;'a)

has structure:

type_tag(x; 'a)

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html