# HG changeset patch
# User blanchet
# Date 1370545928 -7200
# Node ID a11bbb5fef567de0830a7c88974266fe300f08e4
# Parent  74315fe137baa0344adf9bf6b01e3170ff040e93
fixed failure in coinduction rule tactic

diff -r 74315fe137ba -r a11bbb5fef56 src/HOL/BNF/Examples/Misc_Codata.thy
--- a/src/HOL/BNF/Examples/Misc_Codata.thy	Thu Jun 06 15:56:17 2013 +0200
+++ b/src/HOL/BNF/Examples/Misc_Codata.thy	Thu Jun 06 21:12:08 2013 +0200
@@ -1,7 +1,8 @@
 (*  Title:      HOL/BNF/Examples/Misc_Codata.thy
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Andrei Popescu, TU Muenchen
-    Copyright   2012
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2012, 2013
 
 Miscellaneous codatatype declarations.
 *)
@@ -16,6 +17,8 @@
 
 codatatype simple' = X1' unit | X2' unit | X3' unit | X4' unit
 
+codatatype simple'' = X1'' nat int | X2''
+
 codatatype 'a stream = Stream 'a "'a stream"
 
 codatatype 'a mylist = MyNil | MyCons 'a "'a mylist"
diff -r 74315fe137ba -r a11bbb5fef56 src/HOL/BNF/Examples/Misc_Data.thy
--- a/src/HOL/BNF/Examples/Misc_Data.thy	Thu Jun 06 15:56:17 2013 +0200
+++ b/src/HOL/BNF/Examples/Misc_Data.thy	Thu Jun 06 21:12:08 2013 +0200
@@ -17,6 +17,8 @@
 
 datatype_new simple' = X1' unit | X2' unit | X3' unit | X4' unit
 
+datatype_new simple'' = X1'' nat int | X2''
+
 datatype_new 'a mylist = MyNil | MyCons 'a "'a mylist"
 
 datatype_new ('b, 'c, 'd, 'e) some_passive =
diff -r 74315fe137ba -r a11bbb5fef56 src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- 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'