Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
changeset 53570 773302e7741d
parent 53329 c31c0c311cf0
child 53690 a3ad5a0350f9 
--- 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'
isabelle