# HG changeset patch
# User paulson
# Date 886858805 -3600
# Node ID 18a3f33f2097b19e52710d1b300c50ee704b8bb2
# Parent  b1322be47244c0ee519017b28ab6244519c3ceee
moved freeze_thaw to drule.ML

diff -r b1322be47244 -r 18a3f33f2097 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Sat Feb 07 14:39:35 1998 +0100
+++ b/src/Pure/tactic.ML	Sat Feb 07 14:40:05 1998 +0100
@@ -48,7 +48,6 @@
   val fold_tac		: thm list -> tactic
   val forward_tac	: thm list -> int -> tactic   
   val forw_inst_tac	: (string*string)list -> thm -> int -> tactic
-  val freeze_thaw	: thm -> thm * (thm -> thm)
   val insert_tagged_brl : ('a*(bool*thm)) * 
                           (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) ->
                           ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net
@@ -105,31 +104,10 @@
     			 Seq.make(fn()=> seqcell));
 
 
-(*Convert all Vars in a theorem to Frees.  Also return a function for 
-  reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.
-  Similar code in type/freeze_thaw*)
-fun freeze_thaw th =
-  let val fth = freezeT th
-      val {prop,sign,...} = rep_thm fth
-      val used = add_term_names (prop, [])
-      and vars = term_vars prop
-      fun newName (Var(ix,_), (pairs,used)) = 
-	    let val v = variant used (string_of_indexname ix)
-	    in  ((ix,v)::pairs, v::used)  end;
-      val (alist, _) = foldr newName (vars, ([], used))
-      fun mk_inst (Var(v,T)) = 
-	  (cterm_of sign (Var(v,T)),
-	   cterm_of sign (Free(the (assoc(alist,v)), T)))
-      val insts = map mk_inst vars
-      fun thaw th' = 
-	  th' |> forall_intr_list (map #2 insts)
-	      |> forall_elim_list (map #1 insts)
-  in  (instantiate ([],insts) fth, thaw)  end;
-
-
 (*Rotates the given subgoal to be the last.  Useful when re-playing
   an old proof script, when the proof of an early subgoal fails.
-  DOES NOT WORK FOR TYPE VARIABLES.*)
+  DOES NOT WORK FOR TYPE VARIABLES.
+  Similar to drule/rotate_prems*)
 fun defer_tac i state = 
     let val (state',thaw) = freeze_thaw state
 	val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state'))