diff -r afd288caf573 -r 98a2d517cabe src/Pure/logic.ML
--- a/src/Pure/logic.ML	Thu Jun 05 13:29:41 1997 +0200
+++ b/src/Pure/logic.ML	Thu Jun 05 13:30:24 1997 +0200
@@ -20,7 +20,6 @@
   val dest_inclass	: term -> typ * class
   val dest_type		: term -> typ
   val flatten_params	: int -> term -> term
-  val freeze_vars	: term -> term
   val incr_indexes	: typ list * int -> term -> term
   val lift_fns		: term * int -> (term -> term) * (term -> term)
   val list_flexpairs	: (term*term)list * term -> term
@@ -44,7 +43,6 @@
   val strip_imp_prems	: term -> term list
   val strip_params	: term -> (string * typ) list
   val strip_prems	: int * term list * term -> term list * term
-  val thaw_vars		: term -> term
   val unvarify		: term -> term
   val varify		: term -> term
   val termord		: term * term -> order
@@ -174,29 +172,6 @@
 		   A);
 
 
-(*Freeze all (T)Vars by turning them into (T)Frees*)
-fun freeze_vars(Var(ixn,T)) = Free(Syntax.string_of_vname ixn,
-                                   Type.freeze_vars T)
-  | freeze_vars(Const(a,T)) = Const(a,Type.freeze_vars T)
-  | freeze_vars(Free(a,T))  = Free(a,Type.freeze_vars T)
-  | freeze_vars(s$t)        = freeze_vars s $ freeze_vars t
-  | freeze_vars(Abs(a,T,t)) = Abs(a,Type.freeze_vars T,freeze_vars t)
-  | freeze_vars(b)          = b;
-
-(*Reverse the effect of freeze_vars*)
-fun thaw_vars(Const(a,T)) = Const(a,Type.thaw_vars T)
-  | thaw_vars(Free(a,T))  =
-      let val T' = Type.thaw_vars T
-      in case explode a of
-	   "?"::vn => let val (ixn,_) = Syntax.scan_varname vn
-                      in Var(ixn,T') end
-	 | _       => Free(a,T')
-      end
-  | thaw_vars(Abs(a,T,t)) = Abs(a,Type.thaw_vars T, thaw_vars t)
-  | thaw_vars(s$t)        = thaw_vars s $ thaw_vars t
-  | thaw_vars(b)          = b;
-
-
 (*** Specialized operations for resolution... ***)
 
 (*For all variables in the term, increment indexnames and lift over the Us