src/Pure/logic.ML

--- a/src/Pure/logic.ML	Sat Mar 20 02:23:41 2010 +0100
+++ b/src/Pure/logic.ML	Sat Mar 20 17:33:11 2010 +0100
@@ -68,10 +68,10 @@
   val list_rename_params: string list * term -> term
   val assum_pairs: int * term -> (term*term)list
   val assum_problems: int * term -> (term -> term) * term list * term
-  val varifyT: typ -> typ
-  val unvarifyT: typ -> typ
-  val varify: term -> term
-  val unvarify: term -> term
+  val varifyT_global: typ -> typ
+  val unvarifyT_global: typ -> typ
+  val varify_global: term -> term
+  val unvarify_global: term -> term
   val get_goal: term -> int -> term
   val goal_params: term -> int -> term * term list
   val prems_of_goal: term -> int -> term list
@@ -465,35 +465,35 @@
 fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi);
 fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
 
-fun varifyT_same ty = ty
+fun varifyT_global_same ty = ty
   |> Term_Subst.map_atypsT_same
     (fn TFree (a, S) => TVar ((a, 0), S)
       | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
 
-fun unvarifyT_same ty = ty
+fun unvarifyT_global_same ty = ty
   |> Term_Subst.map_atypsT_same
     (fn TVar ((a, 0), S) => TFree (a, S)
       | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
       | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
 
-val varifyT = Same.commit varifyT_same;
-val unvarifyT = Same.commit unvarifyT_same;
+val varifyT_global = Same.commit varifyT_global_same;
+val unvarifyT_global = Same.commit unvarifyT_global_same;
 
-fun varify tm = tm
+fun varify_global tm = tm
   |> Same.commit (Term_Subst.map_aterms_same
     (fn Free (x, T) => Var ((x, 0), T)
       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
       | _ => raise Same.SAME))
-  |> Same.commit (Term_Subst.map_types_same varifyT_same)
+  |> Same.commit (Term_Subst.map_types_same varifyT_global_same)
   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
 
-fun unvarify tm = tm
+fun unvarify_global tm = tm
   |> Same.commit (Term_Subst.map_aterms_same
     (fn Var ((x, 0), T) => Free (x, T)
       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
       | Free (x, _) => raise TERM (bad_fixed x, [tm])
       | _ => raise Same.SAME))
-  |> Same.commit (Term_Subst.map_types_same unvarifyT_same)
+  |> Same.commit (Term_Subst.map_types_same unvarifyT_global_same)
   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);