src/Pure/context.ML

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