# HG changeset patch
# User blanchet
# Date 1473323708 -7200
# Node ID 9321b3d50abdd444bbd3e838e1ed46c887cdf6cf
# Parent  adc6ddabfe459982d31720779dfc3e5e17fcc8f9
made it easier to catch 'empty datatype' exception

diff -r adc6ddabfe45 -r 9321b3d50abd src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 08 10:16:39 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 08 10:35:08 2016 +0200
@@ -2785,11 +2785,12 @@
     lthy
   end;
 
-fun co_datatypes x = define_co_datatypes (K I) (K I) (K I) (K I) x;
-
-fun co_datatype_cmd x =
+fun co_datatypes fp = define_co_datatypes (K I) (K I) (K I) (K I) fp;
+
+fun co_datatype_cmd fp construct_fp options lthy =
   define_co_datatypes Plugin_Name.make_filter Typedecl.read_constraint Syntax.parse_typ
-    Syntax.parse_term x;
+    Syntax.parse_term fp construct_fp options lthy
+  handle EMPTY_DATATYPE s => error ("Cannot define empty datatype " ^ quote s);
 
 val parse_ctr_arg =
   @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"}
diff -r adc6ddabfe45 -r 9321b3d50abd src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Sep 08 10:16:39 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Sep 08 10:35:08 2016 +0200
@@ -10,6 +10,8 @@
 
 signature BNF_FP_UTIL =
 sig
+  exception EMPTY_DATATYPE of string
+
   type fp_result =
     {Ts: typ list,
      bnfs: BNF_Def.bnf list,
@@ -224,6 +226,8 @@
 open BNF_Util
 open BNF_FP_Util_Tactics
 
+exception EMPTY_DATATYPE of string;
+
 type fp_result =
   {Ts: typ list,
    bnfs: bnf list,
diff -r adc6ddabfe45 -r 9321b3d50abd src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 08 10:16:39 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 08 10:35:08 2016 +0200
@@ -171,7 +171,7 @@
     val reachable = fixpoint (op =) enrich [];
     val _ = (case subtract (op =) (map snd reachable) all of
         [] => ()
-      | i :: _ => error ("Cannot define empty datatype " ^ quote (Binding.name_of (nth bs (i - m)))));
+      | i :: _ => raise EMPTY_DATATYPE (Binding.name_of (nth bs (i - m))));
 
     val wit_thms = flat (map2 (fn bnf => fn (j, _) => nth (wit_thmss_of_bnf bnf) j) bnfs reachable);