--- 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;