--- a/src/Pure/Isar/subgoal.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/Isar/subgoal.ML Fri Sep 10 14:59:19 2021 +0200
@@ -14,7 +14,7 @@
sig
type focus =
{context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list,
- concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list}
+ concl: cterm, schematics: ctyp TVars.table * cterm Vars.table}
val focus_params: Proof.context -> int -> binding list option -> thm -> focus * thm
val focus_params_fixed: Proof.context -> int -> binding list option -> thm -> focus * thm
val focus_prems: Proof.context -> int -> binding list option -> thm -> focus * thm
@@ -39,7 +39,7 @@
type focus =
{context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list,
- concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list};
+ concl: cterm, schematics: ctyp TVars.table * cterm Vars.table};
fun gen_focus (do_prems, do_concl) ctxt i bindings raw_st =
let
@@ -56,9 +56,9 @@
val text = asms @ (if do_concl then [concl] else []);
val ((_, inst), ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
- val schematic_terms = Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt3 t)) inst [];
+ val schematic_terms = Vars.map (K (Thm.cterm_of ctxt3)) inst;
- val schematics = (TVars.dest schematic_types, schematic_terms);
+ val schematics = (schematic_types, schematic_terms);
val asms' = map (Thm.instantiate_cterm schematics) asms;
val concl' = Thm.instantiate_cterm schematics concl;
val (prems, context) = Assumption.add_assumes asms' ctxt3;
@@ -100,8 +100,8 @@
in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
val (inst1, inst2) =
split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys));
-
- val th'' = Thm.instantiate ([], map (apfst (Term.dest_Var o Thm.term_of)) inst1) th';
+ val inst = Vars.build (fold (Vars.add o apfst (Term.dest_Var o Thm.term_of)) inst1);
+ val th'' = Thm.instantiate (TVars.empty, inst) th';
in ((inst2, th''), ctxt'') end;
(*