# 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;