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;