1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
     1.3 @@ -52,8 +52,8 @@
     1.4  val iter_or_rec_thms =
     1.5    @{thms sum_map.simps sum.simps(5,6) convol_def case_unit map_pair_def split_conv id_def};
     1.6  
     1.7 -fun mk_iter_or_rec_tac iter_or_rec_defs fld_iter_or_recs ctr_def bnf_map_def ctxt =
     1.8 -  Local_Defs.unfold_tac ctxt (ctr_def :: bnf_map_def :: iter_or_rec_defs @ fld_iter_or_recs) THEN
     1.9 +fun mk_iter_or_rec_tac iter_or_rec_defs fld_iter_or_recs ctr_def pre_map_def ctxt =
    1.10 +  Local_Defs.unfold_tac ctxt (ctr_def :: pre_map_def :: iter_or_rec_defs @ fld_iter_or_recs) THEN
    1.11    Local_Defs.unfold_tac ctxt iter_or_rec_thms THEN rtac refl 1;
    1.12  
    1.13  end;