--- a/src/HOL/Tools/Datatype/datatype.ML Thu Apr 15 12:27:14 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Thu Apr 15 15:38:58 2010 +0200
@@ -682,7 +682,7 @@
(constrs @ [(c, map (dtyp_of_typ new_dts) cargs')],
constr_syntax' @ [(cname, mx')], sorts'')
end handle ERROR msg => cat_error msg
- ("The error above occured in constructor " ^ quote (Binding.str_of cname) ^
+ ("The error above occurred in constructor " ^ quote (Binding.str_of cname) ^
" of datatype " ^ quote (Binding.str_of tname));
val (constrs', constr_syntax', sorts') =