src/Pure/proofterm.ML
changeset 36619 deadcd0ec431
parent 35851 5c5f08f6d6e4
child 36620 e6bb250402b5
     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, []));