src/HOL/Tools/Datatype/datatype.ML

--- a/src/HOL/Tools/Datatype/datatype.ML	Thu Oct 28 22:11:06 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Thu Oct 28 22:12:08 2010 +0200
@@ -703,7 +703,7 @@
     val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
     val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
       if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
-      else raise exn;
+      else reraise exn;
 
     val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);