# HG changeset patch
# User blanchet
# Date 1346836594 -7200
# Node ID ff86a2253f0558128b168b6b80b19fc2d6811bad
# Parent  881e573a619e22bec77da1cb551fb9df03d8bfe4
reindented code

diff -r 881e573a619e -r ff86a2253f05 src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Wed Sep 05 11:11:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Wed Sep 05 11:16:34 2012 +0200
@@ -73,11 +73,11 @@
 
 fun mk_case_eq_tac ctxt exhaust' case_thms disc_thmss' sel_thmss =
   (rtac exhaust' THEN'
-   EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms => EVERY' [
-     hyp_subst_tac THEN'
-     SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)) THEN'
-     rtac case_thm]) case_thms
-  (map (map mk_if_P_or_not_P) (triangle 1 (map (fst o split_last) disc_thmss'))) sel_thmss)) 1;
+   EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms =>
+       EVERY' [hyp_subst_tac THEN'
+         SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)) THEN' rtac case_thm])
+     case_thms (map (map mk_if_P_or_not_P) (triangle 1 (map (fst o split_last) disc_thmss')))
+     sel_thmss)) 1;
 
 fun mk_case_cong_tac exhaust' case_thms =
   (rtac exhaust' THEN'