src/HOL/Tools/inductive_realizer.ML

     in
       if length concls = 1 then lambda x r' else r'
     end
   end;
 
-val nonempty_msg = explode "Nonemptiness check failed for datatype ";
-
 fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) =
   if name = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
   else x;
 
 fun add_dummies f dts used thy =
-  apsnd (pair (map fst dts)) (transform_error (f (map snd dts)) thy)
-  handle ERROR_MESSAGE msg => if nonempty_msg prefix explode msg then
+  apsnd (pair (map fst dts)) (f (map snd dts) thy)
+  handle DatatypeAux.Datatype_Empty name' =>
       let
-        val name = Sign.base_name
-          (implode (drop (length nonempty_msg, explode msg)));
+        val name = Sign.base_name name';
         val dname = variant used "Dummy"
       in add_dummies f (map (add_dummy name dname) dts) (dname :: used) thy
-      end
-    else error msg;
+      end;
 
 fun mk_realizer thy vs params ((rule, rrule), rt) =
   let
     val prems = prems_of rule ~~ prems_of rrule;
     val rvs = map fst (relevant_vars (prop_of rule));

 
     (** datatype representing computational content of inductive set **)
 
     val (thy2, (dummies, dt_info)) = thy1 |>
       (if null dts then rpair ([], None) else
-        apsnd (apsnd Some) o add_dummies (DatatypePackage.add_datatype_i false
+        apsnd (apsnd Some) o add_dummies (DatatypePackage.add_datatype_i false false
           (map #2 dts)) (map (pair false) dts) []) |>>
       Extraction.add_typeof_eqns_i ty_eqs |>>
       Extraction.add_realizes_eqns_i rlz_eqs;
     fun get f x = if_none (apsome f x) [];
     val rec_names = distinct (map (fst o dest_Const o head_of o fst o