--- a/src/Pure/Tools/codegen_data.ML Sat Dec 30 12:41:59 2006 +0100
+++ b/src/Pure/Tools/codegen_data.ML Sat Dec 30 16:08:00 2006 +0100
@@ -426,8 +426,10 @@
let
val k = serial ();
val kind = {name = name, empty = empty, merge = merge, purge = purge};
- val _ = conditional (Datatab.exists (equal name o #name o #2) (! kinds)) (fn () =>
- warning ("Duplicate declaration of code data " ^ quote name));
+ val _ =
+ if Datatab.exists (equal name o #name o #2) (! kinds) then
+ warning ("Duplicate declaration of code data " ^ quote name)
+ else ();
val _ = change kinds (Datatab.update (k, kind));
in k end;