1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Mon Sep 09 14:22:11 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Mon Sep 09 14:23:04 2013 +0200
     1.3 @@ -54,8 +54,8 @@
     1.4  fun mk_primcorec_disc_tac ctxt defs disc k m exclsss =
     1.5    mk_primcorec_prelude ctxt defs disc THEN mk_primcorec_cases_tac ctxt k m exclsss;
     1.6  
     1.7 -fun mk_primcorec_eq_tac ctxt defs sel k m exclsss maps map_idents map_comps =
     1.8 -  mk_primcorec_prelude ctxt defs (sel RS trans) THEN mk_primcorec_cases_tac ctxt k m exclsss THEN
     1.9 +fun mk_primcorec_eq_tac ctxt defs eq_thm k m exclsss maps map_idents map_comps =
    1.10 +  mk_primcorec_prelude ctxt defs (eq_thm RS trans) THEN mk_primcorec_cases_tac ctxt k m exclsss THEN
    1.11    unfold_thms_tac ctxt (@{thms if_if_True if_if_False if_True if_False o_def split_def sum.cases} @
    1.12      maps @ map_comps @ map_idents) THEN HEADGOAL (rtac refl);
    1.13