--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Thu Aug 29 22:56:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Thu Aug 29 23:01:04 2013 +0200
@@ -119,26 +119,26 @@
hyp_subst_tac ctxt ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
(rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI});
-fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_map's pre_set_defs =
+fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_maps pre_set_defs =
HEADGOAL (EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
- SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ set_map's @ sum_prod_thms_set0)),
+ SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ set_maps @ sum_prod_thms_set0)),
solve_prem_prem_tac ctxt]) (rev kks)));
-fun mk_induct_discharge_prem_tac ctxt nn n set_map's pre_set_defs m k kks =
+fun mk_induct_discharge_prem_tac ctxt nn n set_maps pre_set_defs m k kks =
let val r = length kks in
HEADGOAL (EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac ctxt,
REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)]) THEN
EVERY [REPEAT_DETERM_N r
(HEADGOAL (rotate_tac ~1 THEN' dtac meta_mp THEN' rotate_tac 1) THEN prefer_tac 2),
if r > 0 then ALLGOALS Goal.norm_hhf_tac else all_tac, HEADGOAL atac,
- mk_induct_leverage_prem_prems_tac ctxt nn kks set_map's pre_set_defs]
+ mk_induct_leverage_prem_prems_tac ctxt nn kks set_maps pre_set_defs]
end;
-fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' set_map's pre_set_defss =
+fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' set_maps pre_set_defss =
let val n = Integer.sum ns in
unfold_thms_tac ctxt ctr_defs THEN
HEADGOAL (rtac ctor_induct' THEN' inst_as_projs_tac ctxt) THEN
- EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_map's) pre_set_defss
+ EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_maps) pre_set_defss
mss (unflat mss (1 upto n)) kkss)
end;