src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML

   val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
     tactic
   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 ->
     thm list -> thm list -> thm -> int -> int -> thm list list list -> tactic
 end;

 
 val exhaust_inst_as_projs_tac = PRIMITIVE oo exhaust_inst_as_projs;
 
 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'
       cut_tac nchotomy THEN'