--- a/src/Pure/Isar/subgoal.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Pure/Isar/subgoal.ML Sun Jul 05 15:02:30 2015 +0200
@@ -12,8 +12,9 @@
signature SUBGOAL =
sig
- type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
- asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}
+ 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}
val focus_params: Proof.context -> int -> thm -> focus * thm
val focus_params_fixed: Proof.context -> int -> thm -> focus * thm
val focus_prems: Proof.context -> int -> thm -> focus * thm
@@ -36,8 +37,9 @@
(* focus *)
-type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
- asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list};
+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};
fun gen_focus (do_prems, do_concl) ctxt i raw_st =
let
@@ -100,7 +102,7 @@
val (inst1, inst2) =
split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys));
- val th'' = Thm.instantiate ([], inst1) th';
+ val th'' = Thm.instantiate ([], map (apfst (Term.dest_Var o Thm.term_of)) inst1) th';
in ((inst2, th''), ctxt'') end;
(*