src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML

 val split_if_asm = @{thm split_if_asm};
 val split_connectI = @{thms allI impI conjI};
 
 fun mk_primcorec_exhaust_tac n nchotomy =
   let val ks = 1 upto n in
-    HEADGOAL (cut_tac nchotomy THEN'
-     EVERY' (map (fn k =>
-        (if k < n then etac disjE else K all_tac) THEN'
-        REPEAT o (etac conjE THEN' dtac meta_mp THEN' atac) THEN'
-        dtac meta_mp THEN' atac THEN' atac)
-      ks))
+    HEADGOAL (atac ORELSE'
+      cut_tac nchotomy THEN'
+      EVERY' (map (fn k =>
+          (if k < n then etac disjE else K all_tac) THEN'
+          REPEAT o (etac conjE THEN' dtac meta_mp THEN' atac) THEN'
+          dtac meta_mp THEN' atac THEN' atac)
+        ks))
   end;
 
 fun mk_primcorec_assumption_tac ctxt discIs =
   SELECT_GOAL (unfold_thms_tac ctxt
       @{thms not_not not_False_eq_True not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN