# HG changeset patch
# User wenzelm
# Date 1272963770 -7200
# Node ID deadcd0ec431faa52580156f2c0cfe770e34a886
# Parent  7a0990473e0382836bac0c0e01c4a114fa42ad3f
renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);

diff -r 7a0990473e03 -r deadcd0ec431 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue May 04 10:52:43 2010 +0200
+++ b/src/Pure/proofterm.ML	Tue May 04 11:02:50 2010 +0200
@@ -80,7 +80,7 @@
   val implies_intr_proof: term -> proof -> proof
   val forall_intr_proof: term -> string -> proof -> proof
   val varify_proof: term -> (string * sort) list -> proof -> proof
-  val freezeT: term -> proof -> proof
+  val legacy_freezeT: term -> proof -> proof
   val rotate_proof: term list -> term -> int -> proof -> proof
   val permute_prems_prf: term list -> int -> int -> proof -> proof
   val generalize: string list * string list -> int -> proof -> proof
@@ -652,7 +652,7 @@
 
 in
 
-fun freezeT t prf =
+fun legacy_freezeT t prf =
   let
     val used = OldTerm.it_term_types OldTerm.add_typ_tfree_names (t, [])
     and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, []));
diff -r 7a0990473e03 -r deadcd0ec431 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue May 04 10:52:43 2010 +0200
+++ b/src/Pure/thm.ML	Tue May 04 11:02:50 2010 +0200
@@ -1268,7 +1268,7 @@
     val prop2 = Type.legacy_freeze prop1;
     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
   in
-    Thm (deriv_rule1 (Pt.freezeT prop1) der,
+    Thm (deriv_rule1 (Pt.legacy_freezeT prop1) der,
      {thy_ref = thy_ref,
       tags = [],
       maxidx = maxidx_of_term prop2,