src/Pure/Proof/extraction.ML
changeset 16287 7a03b4b4df67
parent 16195 0eb3c15298cd
child 16349 40c5a4d0b3cc
     1.1 --- a/src/Pure/Proof/extraction.ML	Sun Jun 05 23:07:24 2005 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sun Jun 05 23:07:25 2005 +0200
     1.3 @@ -748,8 +748,8 @@
     1.4           NONE =>
     1.5             let
     1.6               val corr_prop = Reconstruct.prop_of prf;
     1.7 -             val ft = fst (Type.freeze_thaw t);
     1.8 -             val fu = fst (Type.freeze_thaw u);
     1.9 +             val ft = Type.freeze t;
    1.10 +             val fu = Type.freeze u;
    1.11               val thy' = if t = nullt then thy else thy |>
    1.12                 Theory.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)] |>
    1.13                 fst o PureThy.add_defs_i false [((extr_name s vs ^ "_def",