src/HOL/Tools/Datatype/datatype.ML
changeset 36148 4ddcc2b07891
parent 35994 9cc3df9a606e
child 36692 54b64d4ad524
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Thu Apr 15 12:27:14 2010 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Thu Apr 15 15:38:58 2010 +0200
     1.3 @@ -682,7 +682,7 @@
     1.4              (constrs @ [(c, map (dtyp_of_typ new_dts) cargs')],
     1.5                constr_syntax' @ [(cname, mx')], sorts'')
     1.6            end handle ERROR msg => cat_error msg
     1.7 -           ("The error above occured in constructor " ^ quote (Binding.str_of cname) ^
     1.8 +           ("The error above occurred in constructor " ^ quote (Binding.str_of cname) ^
     1.9              " of datatype " ^ quote (Binding.str_of tname));
    1.10  
    1.11          val (constrs', constr_syntax', sorts') =