--- a/src/HOL/Tools/datatype_package.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML Sat Jan 14 17:14:06 2006 +0100
@@ -976,8 +976,8 @@
Sign.full_name_path sign tname) (Syntax.const_name cname mx'),
map (dtyp_of_typ new_dts) cargs')],
constr_syntax' @ [(cname, mx')], sorts'')
- end handle ERROR =>
- error ("The error above occured in constructor " ^ cname ^
+ end handle ERROR msg =>
+ cat_error msg ("The error above occured in constructor " ^ cname ^
" of datatype " ^ tname);
val (constrs', constr_syntax', sorts') =