--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Wed Jan 03 11:06:29 2018 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Wed Jan 03 11:06:36 2018 +0100
@@ -74,7 +74,6 @@
val interpret_construction : descr -> (string * sort) list ->
{atyp: typ -> 'a, dtyp: typ list -> int * bool -> string * typ list -> 'a} ->
((string * typ list) * (string * 'a list) list) list
- val check_nonempty : descr list -> unit
val unfold_datatypes : Proof.context -> descr -> info Symtab.table ->
descr -> int -> descr list * int
val find_shortest_path : descr -> int -> (string * int) option
@@ -301,23 +300,6 @@
fun interpD (_, (tyco, dTs, cs)) = ((tyco, map typ_of dTs), map interpC cs);
in map interpD descr end;
-(* nonemptiness check for datatypes *)
-
-fun check_nonempty descr =
- let
- val descr' = flat descr;
- fun is_nonempty_dt is i =
- let
- val (_, _, constrs) = the (AList.lookup (op =) descr' i);
- fun arg_nonempty (_, DtRec i) =
- if member (op =) is i then false
- else is_nonempty_dt (i :: is) i
- | arg_nonempty _ = true;
- in exists (forall (arg_nonempty o strip_dtyp) o snd) constrs 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 _, ...]) *)
(* need to be unfolded *)