--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Thu Mar 05 14:58:35 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Thu Mar 05 15:44:37 2015 +0100
@@ -119,7 +119,7 @@
REPEAT_DETERM o etac conjI THEN' (atac ORELSE' rtac TrueI)
else
rtac FalseE THEN'
- (rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac ORELSE'
+ (rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT o atac ORELSE'
cut_tac fun_disc') THEN'
dresolve_tac ctxt distinct_discs THEN' etac notE THEN' atac)
fun_discss) THEN'