# HG changeset patch
# User blanchet
# Date 1383562748 -3600
# Node ID 357988ad95ec0bb0be6203769750d2b58499f7f4
# Parent  756ff45e08ba466345fc0a8ce2d146e1a57683f4
strengthened tactic

diff -r 756ff45e08ba -r 357988ad95ec src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- 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
diff -r 756ff45e08ba -r 357988ad95ec src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Nov 04 11:03:13 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Nov 04 11:59:08 2013 +0100
@@ -715,8 +715,8 @@
          sel_corecs = sel_corecs}
       end;
 
-    fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) p_is q_isss f_isss f_Tsss
-        coiter_thmsss disc_coitersss sel_coiterssss =
+    fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) p_is q_isss f_isss f_Tsss coiter_thmsss
+        disc_coitersss sel_coiterssss =
       let
         val ctrs = #ctrs (nth ctr_sugars index);
         val discs = #discs (nth ctr_sugars index);