src/Pure/Proof/extraction.ML
changeset 33832 cff42395c246
parent 33704 6aeb8454efc1
child 33955 fff6f11b1f09
     1.1 --- a/src/Pure/Proof/extraction.ML	Sat Nov 21 14:03:36 2009 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sat Nov 21 15:49:29 2009 +0100
     1.3 @@ -310,7 +310,7 @@
     1.4        val vars' = filter_out (fn v =>
     1.5          member (op =) rtypes (tname_of (body_type (fastype_of v)))) vars;
     1.6        val T = etype_of thy' vs [] prop;
     1.7 -      val (T', thw) = Type.freeze_thaw_type
     1.8 +      val (T', thw) = Type.legacy_freeze_thaw_type
     1.9          (if T = nullT then nullT else map fastype_of vars' ---> T);
    1.10        val t = map_types thw (OldGoals.simple_read_term thy' T' s1);
    1.11        val r' = freeze_thaw (condrew thy' eqns
    1.12 @@ -720,8 +720,8 @@
    1.13           NONE =>
    1.14             let
    1.15               val corr_prop = Reconstruct.prop_of prf;
    1.16 -             val ft = Type.freeze t;
    1.17 -             val fu = Type.freeze u;
    1.18 +             val ft = Type.legacy_freeze t;
    1.19 +             val fu = Type.legacy_freeze u;
    1.20               val (def_thms, thy') = if t = nullt then ([], thy) else
    1.21                 thy
    1.22                 |> Sign.add_consts_i [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]