8 (* FIXME proper ML structure! *) |
8 (* FIXME proper ML structure! *) |
9 |
9 |
10 (* FIXME res_inst_tac mostly obsolete, cf. Subgoal.FOCUS *) |
10 (* FIXME res_inst_tac mostly obsolete, cf. Subgoal.FOCUS *) |
11 |
11 |
12 (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) |
12 (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) |
13 fun gen_res_inst_tac_term instf tyinst tinst elim th i st = |
13 fun gen_res_inst_tac_term ctxt instf tyinst tinst elim th i st = |
14 let |
14 let |
15 val thy = theory_of_thm st; |
15 val thy = theory_of_thm st; |
16 val cgoal = nth (cprems_of st) (i - 1); |
16 val cgoal = nth (cprems_of st) (i - 1); |
17 val {maxidx, ...} = rep_cterm cgoal; |
17 val {maxidx, ...} = rep_cterm cgoal; |
18 val j = maxidx + 1; |
18 val j = maxidx + 1; |
25 val th' = instf |
25 val th' = instf |
26 (map (pairself (ctyp_of thy)) tyinst') |
26 (map (pairself (ctyp_of thy)) tyinst') |
27 (map (pairself (cterm_of thy)) tinst') |
27 (map (pairself (cterm_of thy)) tinst') |
28 (Thm.lift_rule cgoal th) |
28 (Thm.lift_rule cgoal th) |
29 in |
29 in |
30 compose_tac (elim, th', nprems_of th) i st |
30 compose_tac ctxt (elim, th', nprems_of th) i st |
31 end handle General.Subscript => Seq.empty; |
31 end handle General.Subscript => Seq.empty; |
32 (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) |
32 (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) |
33 |
33 |
34 val res_inst_tac_term = |
34 fun res_inst_tac_term ctxt = |
35 gen_res_inst_tac_term (curry Thm.instantiate); |
35 gen_res_inst_tac_term ctxt (curry Thm.instantiate); |
36 |
36 |
37 val res_inst_tac_term' = |
37 fun res_inst_tac_term' ctxt = |
38 gen_res_inst_tac_term (K Drule.cterm_instantiate) []; |
38 gen_res_inst_tac_term ctxt (K Drule.cterm_instantiate) []; |
39 |
39 |
40 fun cut_inst_tac_term' ctxt tinst th = |
40 fun cut_inst_tac_term' ctxt tinst th = |
41 res_inst_tac_term' tinst false (Rule_Insts.make_elim_preserve ctxt th); |
41 res_inst_tac_term' ctxt tinst false (Rule_Insts.make_elim_preserve ctxt th); |
42 |
42 |
43 fun get_dyn_thm thy name atom_name = |
43 fun get_dyn_thm thy name atom_name = |
44 Global_Theory.get_thm thy name handle ERROR _ => |
44 Global_Theory.get_thm thy name handle ERROR _ => |
45 error ("The atom type "^atom_name^" is not defined."); |
45 error ("The atom type "^atom_name^" is not defined."); |
46 |
46 |