src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML

--- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Wed Sep 05 15:22:37 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Wed Sep 05 15:40:13 2012 +0200
@@ -89,8 +89,7 @@
 
 fun mk_split_tac exhaust' case_thms injectss distinctsss =
   rtac exhaust' 1 THEN
-  ALLGOALS (fn k =>
-    (hyp_subst_tac THEN'
+  ALLGOALS (fn k => (hyp_subst_tac THEN'
      simp_tac (ss_only (@{thms simp_thms} @ case_thms @ nth injectss (k - 1) @
        flat (nth distinctsss (k - 1))))) k) THEN
   ALLGOALS (blast_tac naked_ctxt);