src/HOL/Tools/datatype_package.ML

     val (dts', constr_syntax, sorts', i) = Library.foldl prep_dt_spec (([], [], [], 0), dts);
     val sorts = sorts' @ (map (rpair (Sign.defaultS sign)) (tyvars \\ map fst sorts'));
     val dt_info = get_datatypes thy;
     val (descr, _) = unfold_datatypes sign dts' sorts dt_info dts' i;
     val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
-      if err then error ("NONEmptiness check failed for datatype " ^ s)
+      if err then error ("Nonemptiness check failed for datatype " ^ s)
       else raise exn;
 
     val descr' = List.concat descr;
     val case_names_induct = mk_case_names_induct descr';
     val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);