renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
authorwenzelm
Tue May 04 11:02:50 2010 +0200 (2010-05-04 ago)
changeset 36619deadcd0ec431
parent 36618 7a0990473e03
child 36620 e6bb250402b5
renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
src/Pure/proofterm.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/proofterm.ML	Tue May 04 10:52:43 2010 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Tue May 04 11:02:50 2010 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4    val implies_intr_proof: term -> proof -> proof
     1.5    val forall_intr_proof: term -> string -> proof -> proof
     1.6    val varify_proof: term -> (string * sort) list -> proof -> proof
     1.7 -  val freezeT: term -> proof -> proof
     1.8 +  val legacy_freezeT: term -> proof -> proof
     1.9    val rotate_proof: term list -> term -> int -> proof -> proof
    1.10    val permute_prems_prf: term list -> int -> int -> proof -> proof
    1.11    val generalize: string list * string list -> int -> proof -> proof
    1.12 @@ -652,7 +652,7 @@
    1.13  
    1.14  in
    1.15  
    1.16 -fun freezeT t prf =
    1.17 +fun legacy_freezeT t prf =
    1.18    let
    1.19      val used = OldTerm.it_term_types OldTerm.add_typ_tfree_names (t, [])
    1.20      and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, []));
     2.1 --- a/src/Pure/thm.ML	Tue May 04 10:52:43 2010 +0200
     2.2 +++ b/src/Pure/thm.ML	Tue May 04 11:02:50 2010 +0200
     2.3 @@ -1268,7 +1268,7 @@
     2.4      val prop2 = Type.legacy_freeze prop1;
     2.5      val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
     2.6    in
     2.7 -    Thm (deriv_rule1 (Pt.freezeT prop1) der,
     2.8 +    Thm (deriv_rule1 (Pt.legacy_freezeT prop1) der,
     2.9       {thy_ref = thy_ref,
    2.10        tags = [],
    2.11        maxidx = maxidx_of_term prop2,