--- 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
--- 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