src/HOL/Tools/Metis/metis_reconstruct.ML
changeset 60781 2da59cdf531c
parent 60642 48dd1cefb4ae
child 60794 f21f70d24844
     1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sat Jul 25 23:15:37 2015 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sat Jul 25 23:41:53 2015 +0200
     1.3 @@ -650,7 +650,7 @@
     1.4                   |> sort (cluster_ord
     1.5                            o apply2 (Meson_Clausify.cluster_of_zapped_var_name
     1.6                                        o fst o fst))
     1.7 -                 |> map (Meson.term_pair_of #> apply2 (Envir.subst_term_types tyenv))
     1.8 +                 |> map (fn (xi, (T, t)) => apply2 (Envir.subst_term_types tyenv) (Var (xi, T), t))
     1.9            val tysubst = tyenv |> Vartab.dest
    1.10          in (tysubst, tsubst) end
    1.11