--- a/src/Pure/context.ML Mon Jul 23 20:47:55 2007 +0200
+++ b/src/Pure/context.ML Mon Jul 23 20:47:56 2007 +0200
@@ -126,7 +126,7 @@
let
val k = serial ();
val kind = {empty = empty, copy = copy, extend = extend, merge = merge};
- val _ = change kinds (Datatab.update (k, kind));
+ val _ = CRITICAL (fn () => change kinds (Datatab.update (k, kind)));
in k end;
val copy_data = Datatab.map' invoke_copy;
@@ -449,7 +449,7 @@
fun declare init =
let
val k = serial ();
- val _ = change kinds (Datatab.update (k, init));
+ val _ = CRITICAL (fn () => change kinds (Datatab.update (k, init)));
in k end;
fun get k dest prf =
@@ -494,8 +494,8 @@
local
val setup_fn = ref (I: theory -> theory);
in
- fun add_setup f = setup_fn := (! setup_fn #> f);
- fun setup () = let val f = ! setup_fn in setup_fn := I; f end;
+ fun add_setup f = CRITICAL (fn () => setup_fn := (! setup_fn #> f));
+ fun setup () = CRITICAL (fn () => let val f = ! setup_fn in setup_fn := I; f end);
end;
end;