# HG changeset patch
# User wenzelm
# Date 1369663058 -7200
# Node ID 6228806b2605b466ea77666279cbef35c13a2984
# Parent  15fcad6eb956207b5c1997cdb3b1e64c758647a5
instantiate types as well (see also Thm.first_order_match);

diff -r 15fcad6eb956 -r 6228806b2605 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon May 27 13:55:04 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon May 27 15:57:38 2013 +0200
@@ -406,10 +406,17 @@
       [] => th
     | pairs =>
         let val thy = theory_of_thm th
-            val (_, tenv) =
+            val cert = cterm_of thy
+            val certT = ctyp_of thy
+            val (tyenv, tenv) =
               fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
-            val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
-            val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
+            fun mkT (v, (S, T)) = (certT (TVar (v, S)), certT T)
+            fun mk (v, (T, t)) =
+              let val T' = Envir.subst_type tyenv T
+              in (cert (Var (v, T')), cert t) end
+            val instsT = Vartab.fold (cons o mkT) tyenv []
+            val insts = Vartab.fold (cons o mk) tenv []
+            val th' = Thm.instantiate (instsT, insts) th
         in  th'  end
         handle THM _ => th;