renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);

--- 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, []));

--- 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,