src/Pure/logic.ML

--- a/src/Pure/logic.ML	Fri Mar 21 12:14:33 2014 +0100
+++ b/src/Pure/logic.ML	Fri Mar 21 12:34:50 2014 +0100
@@ -208,9 +208,9 @@
 
 (** types as terms **)
 
-fun mk_type ty = Const ("TYPE", Term.itselfT ty);
+fun mk_type ty = Const ("Pure.type", Term.itselfT ty);
 
-fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
+fun dest_type (Const ("Pure.type", Type ("itself", [ty]))) = ty
   | dest_type t = raise TERM ("dest_type", [t]);
 
 fun type_map f = dest_type o f o mk_type;