src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
changeset 52323 a11bbb5fef56
parent 52231 cc30c4eb4ec9
child 52324 095c88b93e8d
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Thu Jun 06 15:56:17 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Thu Jun 06 21:12:08 2013 +0200
@@ -161,7 +161,8 @@
   (atac ORELSE' REPEAT o etac conjE THEN'
      full_simp_tac
        (ss_only (@{thm prod.inject} :: no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN_MAYBE'
-     REPEAT o hyp_subst_tac ctxt THEN' REPEAT o rtac conjI THEN' REPEAT o rtac refl);
+     (REPEAT o etac conjE THEN' REPEAT o hyp_subst_tac ctxt) THEN'
+     REPEAT o rtac conjI THEN' REPEAT o rtac refl);
 
 fun mk_coinduct_distinct_ctrs ctxt discs discs' =
   hyp_subst_tac ctxt THEN' REPEAT o etac conjE THEN'