src/Pure/thm.ML
changeset 33832 cff42395c246
parent 33722 e588744f14da
child 33955 fff6f11b1f09
     1.1 --- a/src/Pure/thm.ML	Sat Nov 21 14:03:36 2009 +0100
     1.2 +++ b/src/Pure/thm.ML	Sat Nov 21 15:49:29 2009 +0100
     1.3 @@ -1267,7 +1267,7 @@
     1.4  fun freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) =
     1.5    let
     1.6      val prop1 = attach_tpairs tpairs prop;
     1.7 -    val prop2 = Type.freeze prop1;
     1.8 +    val prop2 = Type.legacy_freeze prop1;
     1.9      val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
    1.10    in
    1.11      Thm (deriv_rule1 (Pt.freezeT prop1) der,