# HG changeset patch
# User blanchet
# Date 1346867870 -7200
# Node ID 766a09b8456234b4704423277925306aa18e1a5a
# Parent  68623861e0f27d908ad47cfe7415a9b80cd62a15
code indentation

diff -r 68623861e0f2 -r 766a09b84562 src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Wed Sep 05 16:17:53 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Wed Sep 05 19:57:50 2012 +0200
@@ -97,8 +97,6 @@
 val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
 
 fun mk_split_asm_tac ctxt split =
-  rtac (split RS trans) 1 THEN
-  Local_Defs.unfold_tac ctxt split_asm_thms THEN
-  rtac refl 1;
+  rtac (split RS trans) 1 THEN Local_Defs.unfold_tac ctxt split_asm_thms THEN rtac refl 1;
 
 end;