--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Wed Sep 25 09:35:37 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Wed Sep 25 10:17:18 2013 +0200
@@ -85,10 +85,10 @@
EVERY (map2 (mk_primcorec_code_of_ctr_case_tac ctxt eq_caseIs) ms ctr_thms);
fun mk_primcorec_code_tac eq_caseIs disc_excludes raw collapses =
- HEADGOAL (rtac (raw RS trans) THEN'
- REPEAT o (resolve_tac (maps (fn thm => [thm, thm RS sym]) (@{thm eq_ifI} :: eq_caseIs)) ORELSE'
- rtac refl ORELSE' (etac notE THEN' atac) ORELSE'
- (dresolve_tac disc_excludes THEN' etac notE THEN' atac) ORELSE'
- eresolve_tac (maps (fn thm => [thm, thm RS sym]) collapses)));
+ HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' REPEAT o
+ (resolve_tac (maps (fn thm => [thm, thm RS sym]) (@{thm eq_ifI} :: eq_caseIs)) ORELSE'
+ rtac refl ORELSE' etac notE THEN' atac ORELSE'
+ dresolve_tac disc_excludes THEN' etac notE THEN' atac ORELSE'
+ eresolve_tac (maps (fn thm => [thm, thm RS sym]) collapses)));
end;