# HG changeset patch
# User lcp
# Date 794919501 -3600
# Node ID 812ccc91bfa0babf50e7c311fb489d7a23360c9b
# Parent  c0f4ae3fda92a0c9fe4aeb276ad1681c910268e1
Put freeze into the signature TACTIC for export

diff -r c0f4ae3fda92 -r 812ccc91bfa0 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Fri Mar 10 10:20:18 1995 +0100
+++ b/src/Pure/tactic.ML	Sat Mar 11 11:58:21 1995 +0100
@@ -45,6 +45,7 @@
   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: thm -> thm   
   val is_fact: thm -> bool
   val lessb: (bool * thm) * (bool * thm) -> bool
   val lift_inst_rule: thm * int * (string*string)list * thm -> thm
@@ -99,7 +100,7 @@
 fun string_of (a,0) = a
   | string_of (a,i) = a ^ "_" ^ string_of_int i;
 
-(*convert all Vars in a theorem to Frees -- export??*)
+(*convert all Vars in a theorem to Frees*)
 fun freeze th =
   let val fth = freezeT th
       val {prop,sign,...} = rep_thm fth