Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Metis/metis_reconstruct.ML
changeset 60781 2da59cdf531c
parent 60642 48dd1cefb4ae
child 60794 f21f70d24844 
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sat Jul 25 23:15:37 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sat Jul 25 23:41:53 2015 +0200
@@ -650,7 +650,7 @@
                  |> sort (cluster_ord
                           o apply2 (Meson_Clausify.cluster_of_zapped_var_name
                                       o fst o fst))
-                 |> map (Meson.term_pair_of #> apply2 (Envir.subst_term_types tyenv))
+                 |> map (fn (xi, (T, t)) => apply2 (Envir.subst_term_types tyenv) (Var (xi, T), t))
           val tysubst = tyenv |> Vartab.dest
         in (tysubst, tsubst) end
isabelle