# HG changeset patch
# User blanchet
# Date 1514973996 -3600
# Node ID 51a7c90fbf19107f219d602d32e06d015d1b8583
# Parent  ac0b81ca3ed5955318ef55f80b673622e3297f69
removed dead code

diff -r ac0b81ca3ed5 -r 51a7c90fbf19 src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
--- 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                                         *)