src/Pure/logic.ML

--- a/src/Pure/logic.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/logic.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -555,7 +555,7 @@
     (fn Free (x, T) => Var ((x, 0), T)
       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
       | t => t)
-  |> Term.map_term_types varifyT
+  |> Term.map_types varifyT
   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
 
 fun unvarify tm =
@@ -564,7 +564,7 @@
       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
       | Free (x, _) => raise TERM (bad_fixed x, [tm])
       | t => t)
-  |> Term.map_term_types unvarifyT
+  |> Term.map_types unvarifyT
   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
 
 val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);
@@ -572,11 +572,11 @@
 
 val legacy_varify =
   Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #>
-  Term.map_term_types legacy_varifyT;
+  Term.map_types legacy_varifyT;
 
 val legacy_unvarify =
   Term.map_aterms (fn Var ((x, 0), T) => Free (x, T) | t => t) #>
-  Term.map_term_types legacy_unvarifyT;
+  Term.map_types legacy_unvarifyT;
 
 
 (* goal states *)