Term.itselfT;

--- a/src/HOL/Tools/typedef_package.ML	Sun Apr 09 19:41:30 2006 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Mon Apr 10 00:33:49 2006 +0200
@@ -128,7 +128,7 @@
     val newT = Type (full_tname, map TFree lhs_tfrees);
 
     val (Rep_name, Abs_name) = if_none opt_morphs ("Rep_" ^ name, "Abs_" ^ name);
-    val setT' = map itselfT args_setT ---> setT;
+    val setT' = map Term.itselfT args_setT ---> setT;
     val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT);
     val RepC = Const (full Rep_name, newT --> oldT);
     val AbsC = Const (full Abs_name, oldT --> newT);

--- a/src/Pure/Proof/extraction.ML	Sun Apr 09 19:41:30 2006 +0200
+++ b/src/Pure/Proof/extraction.ML	Mon Apr 10 00:33:49 2006 +0200
@@ -49,7 +49,7 @@
 val nullt = Const ("Null", nullT);
 
 fun mk_typ T =
-  Const ("Type", itselfT T --> Type ("Type", [])) $ Logic.mk_type T;
+  Const ("Type", Term.itselfT T --> Type ("Type", [])) $ Logic.mk_type T;
 
 fun typeof_proc defaultS vs (Const ("typeof", _) $ u) =
       SOME (mk_typ (case strip_comb u of

--- a/src/Pure/Proof/proof_syntax.ML	Sun Apr 09 19:41:30 2006 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Mon Apr 10 00:33:49 2006 +0200
@@ -181,7 +181,7 @@
 val MinProoft = Const ("MinProof", proofT);
 
 val mk_tyapp = Library.foldl (fn (prf, T) => Const ("Appt",
-  [proofT, itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
+  [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
 
 fun term_of _ (PThm ((name, _), _, _, NONE)) =
       Const (NameSpace.append "thm" name, proofT)

--- a/src/Pure/logic.ML	Sun Apr 09 19:41:30 2006 +0200
+++ b/src/Pure/logic.ML	Mon Apr 10 00:33:49 2006 +0200
@@ -172,7 +172,7 @@
 
 (** types as terms **)
 
-fun mk_type ty = Const ("TYPE", itselfT ty);
+fun mk_type ty = Const ("TYPE", Term.itselfT ty);
 
 fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
   | dest_type t = raise TERM ("dest_type", [t]);
@@ -187,7 +187,7 @@
   handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
 
 fun mk_inclass (ty, c) =
-  Const (const_of_class c, itselfT ty --> propT) $ mk_type ty;
+  Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
 
 fun dest_inclass (t as Const (c_class, _) $ ty) =
       ((dest_type ty, class_of_const c_class)

--- a/src/Pure/pure_thy.ML	Sun Apr 09 19:41:30 2006 +0200
+++ b/src/Pure/pure_thy.ML	Mon Apr 10 00:33:49 2006 +0200
@@ -624,7 +624,7 @@
     [Const ("==", [aT, aT] ---> propT),
      Const ("==>", [propT, propT] ---> propT),
      Const ("all", (aT --> propT) --> propT),
-     Const ("TYPE", a_itselfT),
+     Const ("TYPE", Term.a_itselfT),
      Const (Term.dummy_patternN, aT)]
   |> Theory.add_trfuns Syntax.pure_trfuns
   |> Theory.add_trfunsT Syntax.pure_trfunsT

--- a/src/Pure/sign.ML	Sun Apr 09 19:41:30 2006 +0200
+++ b/src/Pure/sign.ML	Mon Apr 10 00:33:49 2006 +0200
@@ -813,7 +813,7 @@
       val syn' = Syntax.extend_consts [bclass] syn;
       val tsig' = Type.add_classes (pp thy) naming [(bclass, classes)] tsig;
     in (naming, syn', tsig', consts) end)
-  |> add_consts_i [(Logic.const_of_class bclass, a_itselfT --> propT, NoSyn)];
+  |> add_consts_i [(Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
 
 val add_classes = fold (gen_add_class intern_class);
 val add_classes_i = fold (gen_add_class (K I));