# HG changeset patch
# User berghofe
# Date 1086715433 -7200
# Node ID 4938ce4ef295f3962c7c48a5ac950da86f1ecec4
# Parent  b792081d2399c4607febec1658fba3d8a0bae70a
Added exception Datatype_Empty.

diff -r b792081d2399 -r 4938ce4ef295 src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Tue Jun 08 19:22:37 2004 +0200
+++ b/src/HOL/Tools/datatype_aux.ML	Tue Jun 08 19:23:53 2004 +0200
@@ -43,6 +43,7 @@
   type datatype_info
 
   exception Datatype
+  exception Datatype_Empty of string
   val name_of_typ : typ -> string
   val dtyp_of_typ : (string * string list) list -> typ -> dtyp
   val mk_Free : string -> typ -> int -> term
@@ -203,6 +204,7 @@
   | subst_DtTFree i _ (DtRec j) = DtRec (i + j);
 
 exception Datatype;
+exception Datatype_Empty of string;
 
 fun dest_DtTFree (DtTFree a) = a
   | dest_DtTFree _ = raise Datatype;
@@ -284,7 +286,7 @@
       in exists ((forall (arg_nonempty o strip_dtyp)) o snd) constrs
       end
   in assert_all (fn (i, _) => is_nonempty_dt [i] i) (hd descr)
-    (fn (_, (s, _, _)) => "Nonemptiness check failed for datatype " ^ s)
+    (fn (_, (s, _, _)) => raise Datatype_Empty s)
   end;
 
 (* unfold a list of mutually recursive datatype specifications *)
diff -r b792081d2399 -r 4938ce4ef295 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Tue Jun 08 19:22:37 2004 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Tue Jun 08 19:23:53 2004 +0200
@@ -29,7 +29,7 @@
        induction : thm,
        size : thm list,
        simps : thm list}
-  val add_datatype_i : bool -> string list -> (string list * bstring * mixfix *
+  val add_datatype_i : bool -> bool -> string list -> (string list * bstring * mixfix *
     (bstring * typ list * mixfix) list) list -> theory -> theory *
       {distinct : thm list list,
        inject : thm list list,
@@ -904,7 +904,7 @@
 
 (******************************** add datatype ********************************)
 
-fun gen_add_datatype prep_typ flat_names new_type_names dts thy =
+fun gen_add_datatype prep_typ err flat_names new_type_names dts thy =
   let
     val _ = Theory.requires thy "Datatype_Universe" "datatype definitions";
 
@@ -963,7 +963,9 @@
     val sorts = sorts' @ (map (rpair (Sign.defaultS sign)) (tyvars \\ map fst sorts'));
     val dt_info = get_datatypes thy;
     val (descr, _) = unfold_datatypes sign dts' sorts dt_info dts' i;
-    val _ = check_nonempty descr;
+    val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
+      if err then error ("Nonemptiness check failed for datatype " ^ s)
+      else raise exn;
 
     val descr' = flat descr;
     val case_names_induct = mk_case_names_induct descr';
@@ -975,7 +977,7 @@
   end;
 
 val add_datatype_i = gen_add_datatype cert_typ;
-val add_datatype = gen_add_datatype read_typ;
+val add_datatype = gen_add_datatype read_typ true;
 
 
 (** package setup **)