# HG changeset patch
# User blanchet
# Date 1388754277 -3600
# Node ID c63223067cab92509a375141e8047de02195bfa6
# Parent  44373f3560c7810d0adbda58c78193bb68a04858
strengthened tactic

diff -r 44373f3560c7 -r c63223067cab src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 03 13:55:34 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 03 14:04:37 2014 +0100
@@ -960,15 +960,9 @@
         de_facto_exhaustives disc_eqnss
       |> list_all_fun_args []
     val nchotomy_taut_thmss =
-      map3 (fn {disc_exhausts, ...} => fn syntactic_exhaustive =>
-          (case maybe_tac of
-            SOME tac => map_prove_with_tac tac
-          | NONE =>
-            if syntactic_exhaustive then
-              map_prove_with_tac (fn {context = ctxt, ...} =>
-                mk_primcorec_nchotomy_tac ctxt disc_exhausts)
-            else
-              K []))
+      map3 (fn {disc_exhausts, ...} => fn false => K []
+          | true => map_prove_with_tac (fn {context = ctxt, ...} =>
+              mk_primcorec_nchotomy_tac ctxt disc_exhausts))
         corec_specs syntactic_exhaustives nchotomy_goalss;
     val goalss = goalss'
       |> (if is_none maybe_tac then
diff -r 44373f3560c7 -r c63223067cab src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Fri Jan 03 13:55:34 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Fri Jan 03 14:04:37 2014 +0100
@@ -55,7 +55,7 @@
   eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac;
 
 fun mk_primcorec_nchotomy_tac ctxt disc_exhausts =
-  HEADGOAL (clean_blast_tac ctxt);
+  HEADGOAL (Method.insert_tac disc_exhausts THEN' clean_blast_tac ctxt);
 
 fun mk_primcorec_exhaust_tac ctxt frees n nchotomy =
   let val ks = 1 upto n in