made tactic handle gracefully the case: codatatype ('a, 's) scheduler2 = Combine2 "'s => 'a" "'s => ('a, 's) scheduler2"
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Thu Sep 12 17:18:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Thu Sep 12 17:36:06 2013 +0200
@@ -152,7 +152,7 @@
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);
+ REPEAT o (rtac refl ORELSE' atac));
fun mk_coinduct_distinct_ctrs_tac ctxt discs discs' =
hyp_subst_tac ctxt THEN' REPEAT o etac conjE THEN'