# HG changeset patch
# User blanchet
# Date 1388753734 -3600
# Node ID 44373f3560c7810d0adbda58c78193bb68a04858
# Parent  ffed2452f5f6932857b15497a378d0b2a8fb5f9c
refactoring

diff -r ffed2452f5f6 -r 44373f3560c7 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 03 11:26:44 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 03 13:55:34 2014 +0100
@@ -77,6 +77,7 @@
 
 type corec_spec =
   {corec: term,
+   disc_exhausts: thm list,
    nested_map_idents: thm list,
    nested_map_comps: thm list,
    ctr_specs: corec_ctr_spec list};
@@ -443,6 +444,7 @@
           disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...} : fp_sugar)
         p_is q_isss f_isss f_Tsss =
       {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)),
+       disc_exhausts = #disc_exhausts (nth ctr_sugars index),
        nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs,
        nested_map_comps = map map_comp_of_bnf nested_bnfs,
        ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss
@@ -958,15 +960,16 @@
         de_facto_exhaustives disc_eqnss
       |> list_all_fun_args []
     val nchotomy_taut_thmss =
-      map2 (fn syntactic_exhaustive =>
+      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, ...} => HEADGOAL (clean_blast_tac ctxt))
+              map_prove_with_tac (fn {context = ctxt, ...} =>
+                mk_primcorec_nchotomy_tac ctxt disc_exhausts)
             else
               K []))
-        syntactic_exhaustives nchotomy_goalss;
+        corec_specs syntactic_exhaustives nchotomy_goalss;
     val goalss = goalss'
       |> (if is_none maybe_tac then
           append (map2 (fn true => K [] | false => map (rpair [])) syntactic_exhaustives
@@ -1291,6 +1294,6 @@
   lthy
   |> after_qed (map (fn [] => []
       | _ => primcorec_error "need exclusiveness proofs - use primcorecursive instead of primcorec")
-    goalss)) ooo add_primcorec_ursive_cmd (SOME (fn {context = ctxt, ...} => auto_tac ctxt));
+    goalss)) ooo add_primcorec_ursive_cmd (SOME (auto_tac o #context));
 
 end;
diff -r ffed2452f5f6 -r 44373f3560c7 src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Fri Jan 03 11:26:44 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Fri Jan 03 13:55:34 2014 +0100
@@ -15,6 +15,7 @@
   val mk_primcorec_disc_iff_tac: Proof.context -> string list -> thm -> thm -> thm list list ->
     thm list -> tactic
   val mk_primcorec_exhaust_tac: Proof.context -> string list -> int -> thm -> tactic
+  val mk_primcorec_nchotomy_tac: Proof.context -> thm list -> tactic
   val mk_primcorec_raw_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list ->
     thm list -> int list -> thm list -> thm option -> tactic
   val mk_primcorec_sel_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
@@ -53,6 +54,9 @@
 fun distinct_in_prems_tac distincts =
   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);
+
 fun mk_primcorec_exhaust_tac ctxt frees n nchotomy =
   let val ks = 1 upto n in
     HEADGOAL (atac ORELSE'