src/HOL/Tools/datatype_aux.ML
changeset 14887 4938ce4ef295
parent 14673 3d760a971fde
child 14981 e73f8140af78
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Tue Jun 08 19:22:37 2004 +0200
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Tue Jun 08 19:23:53 2004 +0200
     1.3 @@ -43,6 +43,7 @@
     1.4    type datatype_info
     1.5  
     1.6    exception Datatype
     1.7 +  exception Datatype_Empty of string
     1.8    val name_of_typ : typ -> string
     1.9    val dtyp_of_typ : (string * string list) list -> typ -> dtyp
    1.10    val mk_Free : string -> typ -> int -> term
    1.11 @@ -203,6 +204,7 @@
    1.12    | subst_DtTFree i _ (DtRec j) = DtRec (i + j);
    1.13  
    1.14  exception Datatype;
    1.15 +exception Datatype_Empty of string;
    1.16  
    1.17  fun dest_DtTFree (DtTFree a) = a
    1.18    | dest_DtTFree _ = raise Datatype;
    1.19 @@ -284,7 +286,7 @@
    1.20        in exists ((forall (arg_nonempty o strip_dtyp)) o snd) constrs
    1.21        end
    1.22    in assert_all (fn (i, _) => is_nonempty_dt [i] i) (hd descr)
    1.23 -    (fn (_, (s, _, _)) => "Nonemptiness check failed for datatype " ^ s)
    1.24 +    (fn (_, (s, _, _)) => raise Datatype_Empty s)
    1.25    end;
    1.26  
    1.27  (* unfold a list of mutually recursive datatype specifications *)