# HG changeset patch
# User wenzelm
# Date 1288296728 -7200
# Node ID 96fff8c0a85364b6f2da22f40f284b306317f9ca
# Parent  8694a12611f9bfe6df8c594a37905c94612b9c8b
preserve original source position of exn;

diff -r 8694a12611f9 -r 96fff8c0a853 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);