src/Pure/Proof/extraction.ML

     fun add_def (s, (vs, ((t, u), (prf, _)))) thy =
       (case Sign.const_type (sign_of thy) (extr_name s vs) of
          NONE =>
            let
              val corr_prop = Reconstruct.prop_of prf;
-             val ft = fst (Type.freeze_thaw t);
-             val fu = fst (Type.freeze_thaw u);
+             val ft = Type.freeze t;
+             val fu = Type.freeze u;
              val thy' = if t = nullt then thy else thy |>
                Theory.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)] |>
                fst o PureThy.add_defs_i false [((extr_name s vs ^ "_def",
                  Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])];
            in