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