# HG changeset patch
# User berghofe
# Date 1086715527 -7200
# Node ID 99ac3eb0f84ee7e5313a4272293225d98ceabd98
# Parent  4938ce4ef295f3962c7c48a5ac950da86f1ecec4
add_dummies no longer uses transform_error but handles specific
exception Datatype_Empty instead.

diff -r 4938ce4ef295 -r 99ac3eb0f84e src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Jun 08 19:23:53 2004 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jun 08 19:25:27 2004 +0200
@@ -234,22 +234,18 @@
     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
@@ -312,7 +308,7 @@
 
     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;