# HG changeset patch
# User wenzelm
# Date 1630691757 -7200
# Node ID 291e71ed0174295baae58d3296f60cf5f8a930f1
# Parent  c49134ee16c1f9bd82f3f888732d6ad0f4696dbb
proper inst table;

diff -r c49134ee16c1 -r 291e71ed0174 src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Fri Sep 03 18:57:33 2021 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Fri Sep 03 19:55:57 2021 +0200
@@ -451,8 +451,9 @@
     val ({context = ctxt', concl, params, prems, asms, schematics}, goal') =
       Subgoal.focus_params ctxt i bindings goal;
 
-    val (inst, ctxt'') = Variable.import_inst true [Thm.term_of concl] ctxt';
-    val schematic_terms = map (apsnd (Thm.cterm_of ctxt'')) (#2 inst);
+    val ((_, inst), ctxt'') = Variable.import_inst true [Thm.term_of concl] ctxt';
+    val schematic_terms =
+      Term_Subst.Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt'' t)) inst [];
 
     val goal'' = Thm.instantiate ([], schematic_terms) goal';
     val concl' = Thm.instantiate_cterm ([], schematic_terms) concl;