1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Fri Aug 30 14:07:49 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Fri Aug 30 14:17:19 2013 +0200
     1.3 @@ -94,17 +94,17 @@
     1.4    @{thms comp_def convol_def fst_conv id_def prod_case_Pair_iden snd_conv
     1.5        split_conv unit_case_Unity} @ sum_prod_thms_map;
     1.6  
     1.7 -fun mk_iter_tac pre_map_defs map_id's iter_defs ctor_iter ctr_def ctxt =
     1.8 -  unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_id's @
     1.9 +fun mk_iter_tac pre_map_defs map_idents iter_defs ctor_iter ctr_def ctxt =
    1.10 +  unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_idents @
    1.11      iter_unfold_thms) THEN HEADGOAL (rtac refl);
    1.12  
    1.13  val coiter_unfold_thms = @{thms id_def} @ sum_prod_thms_map;
    1.14  
    1.15 -fun mk_coiter_tac coiter_defs map_id's ctor_dtor_coiter pre_map_def ctr_def ctxt =
    1.16 +fun mk_coiter_tac coiter_defs map_idents ctor_dtor_coiter pre_map_def ctr_def ctxt =
    1.17    unfold_thms_tac ctxt (ctr_def :: coiter_defs) THEN
    1.18    HEADGOAL (rtac (ctor_dtor_coiter RS trans) THEN'
    1.19      asm_simp_tac (put_simpset ss_if_True_False ctxt)) THEN_MAYBE
    1.20 -  (unfold_thms_tac ctxt (pre_map_def :: map_id's @ coiter_unfold_thms) THEN
    1.21 +  (unfold_thms_tac ctxt (pre_map_def :: map_idents @ coiter_unfold_thms) THEN
    1.22     HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong)));
    1.23  
    1.24  fun mk_disc_coiter_iff_tac case_splits' coiters discs ctxt =