1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 26 16:25:12 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 26 16:41:32 2013 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4  fun mk_primcorec_assumption_tac ctxt discIs =
     1.5    HEADGOAL (SELECT_GOAL (unfold_thms_tac ctxt
     1.6        @{thms not_not not_False_eq_True de_Morgan_conj de_Morgan_disj} THEN
     1.7 -    SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE'
     1.8 +    SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE'
     1.9      resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE'
    1.10      dresolve_tac discIs THEN' atac)))));
    1.11