# HG changeset patch
# User blanchet
# Date 1389361177 -3600
# Node ID 5747fdd4ad3b8cb4b0a8afe24e2e8e7eaa8205d0
# Parent  b4b82802588017071a786cbbedc1f41915cf6835
fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')

diff -r b4b828025880 -r 5747fdd4ad3b src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 14:39:37 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 14:39:37 2014 +0100
@@ -989,9 +989,14 @@
         de_facto_exhaustives disc_eqnss
       |> list_all_fun_args []
     val nchotomy_taut_thmss =
-      map3 (fn {disc_exhausts, ...} => fn false => K []
-          | true => map_prove_with_tac (fn {context = ctxt, ...} =>
-              mk_primcorec_nchotomy_tac ctxt disc_exhausts))
+      map3 (fn {disc_exhausts, ...} => fn syntactic_exhaustive =>
+          if syntactic_exhaustive then
+            map_prove_with_tac (fn {context = ctxt, ...} =>
+              mk_primcorec_nchotomy_tac ctxt disc_exhausts)
+          else
+            (case tac_opt of
+              SOME tac => map_prove_with_tac tac
+            | NONE => K []))
         corec_specs syntactic_exhaustives nchotomy_goalss;
     val goalss = goalss'
       |> (if is_none tac_opt then
@@ -1004,9 +1009,11 @@
       let
         val def_thms = map (snd o snd) def_thms';
 
-        val nchotomy_thmss = nchotomy_taut_thmss
-          |> (if is_none tac_opt then map2 append (take actual_nn thmss'') else I);
-        val exclude_thmss = thmss'' |> is_none tac_opt ? drop actual_nn;
+        val (nchotomy_thmss, exclude_thmss) =
+          if is_none tac_opt then
+            (map2 append (take actual_nn thmss'') nchotomy_taut_thmss, drop actual_nn thmss'')
+          else
+            (nchotomy_taut_thmss, thmss'');
 
         val ps =
           Variable.variant_frees lthy (maps (maps #fun_args) disc_eqnss) [("P", HOLogic.boolT)];
@@ -1329,7 +1336,7 @@
 val add_primcorec_cmd = (fn (goalss, after_qed, lthy) =>
   lthy
   |> after_qed (map (fn [] => []
-      | _ => primcorec_error "need exclusiveness proofs - use primcorecursive instead of primcorec")
+      | _ => error "\"auto\" failed -- use \"primcorecursive\" instead of \"primcorec\"")
     goalss)) ooo add_primcorec_ursive_cmd (SOME (auto_tac o #context));
 
 end;