author | blanchet |
Wed, 05 Sep 2012 19:57:50 +0200 | |
changeset 49168 | 766a09b84562 |
parent 49167 | 68623861e0f2 |
child 49169 | 937a0fadddfb |
--- 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;