--- a/src/HOL/Tools/Datatype/datatype_aux.ML Sun Aug 10 15:16:01 2014 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Sun Aug 10 15:45:06 2014 +0200
@@ -311,10 +311,9 @@
else is_nonempty_dt (i :: is) i
| arg_nonempty _ = true;
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, _, _)) => raise Datatype_Empty s)
- end;
+ val _ = hd descr |> forall (fn (i, (s, _, _)) =>
+ is_nonempty_dt [i] i orelse raise Datatype_Empty s)
+ in () end;
(* unfold a list of mutually recursive datatype specifications *)
(* all types of the form DtType (dt_name, [..., DtRec _, ...]) *)