--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Mon Nov 04 11:03:13 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Mon Nov 04 11:59:08 2013 +0100
@@ -151,8 +151,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'
- REPEAT o etac conjE THEN_MAYBE' REPEAT o hyp_subst_tac ctxt THEN' REPEAT o rtac conjI THEN'
- REPEAT o (rtac refl ORELSE' atac));
+ REPEAT o etac conjE THEN_MAYBE' REPEAT o hyp_subst_tac ctxt THEN'
+ REPEAT o (resolve_tac [refl, conjI] ORELSE' atac));
fun mk_coinduct_distinct_ctrs_tac ctxt discs discs' =
let