diff -r 7e291ae244ea -r 985f8b49c050 src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Fri Nov 29 14:24:21 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Sun Dec 01 19:32:57 2013 +0100
@@ -13,7 +13,7 @@
   val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
     tactic
   val mk_primcorec_raw_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list ->
-    thm list -> int list -> thm list -> tactic
+    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;
@@ -116,7 +116,8 @@
        (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))))
   end;
 
-fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms f_ctrs =
+(* TODO: implement "exhaustive" (maybe_exh) *)
+fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms f_ctrs maybe_exh =
   EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms) ms
     f_ctrs) THEN
   IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN