diff -r 8d34e64eeaf6 -r 279b129498b6 src/Pure/Tools/codegen_data.ML
--- 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;