src/Pure/context.ML
changeset 23944 2ea068548a83
parent 23595 7ca68a2c8575
child 24141 73baca986087
     1.1 --- a/src/Pure/context.ML	Mon Jul 23 20:47:55 2007 +0200
     1.2 +++ b/src/Pure/context.ML	Mon Jul 23 20:47:56 2007 +0200
     1.3 @@ -126,7 +126,7 @@
     1.4    let
     1.5      val k = serial ();
     1.6      val kind = {empty = empty, copy = copy, extend = extend, merge = merge};
     1.7 -    val _ = change kinds (Datatab.update (k, kind));
     1.8 +    val _ = CRITICAL (fn () => change kinds (Datatab.update (k, kind)));
     1.9    in k end;
    1.10  
    1.11  val copy_data = Datatab.map' invoke_copy;
    1.12 @@ -449,7 +449,7 @@
    1.13  fun declare init =
    1.14    let
    1.15      val k = serial ();
    1.16 -    val _ = change kinds (Datatab.update (k, init));
    1.17 +    val _ = CRITICAL (fn () => change kinds (Datatab.update (k, init)));
    1.18    in k end;
    1.19  
    1.20  fun get k dest prf =
    1.21 @@ -494,8 +494,8 @@
    1.22  local
    1.23    val setup_fn = ref (I: theory -> theory);
    1.24  in
    1.25 -  fun add_setup f = setup_fn := (! setup_fn #> f);
    1.26 -  fun setup () = let val f = ! setup_fn in setup_fn := I; f end;
    1.27 +  fun add_setup f = CRITICAL (fn () => setup_fn := (! setup_fn #> f));
    1.28 +  fun setup () = CRITICAL (fn () => let val f = ! setup_fn in setup_fn := I; f end);
    1.29  end;
    1.30  
    1.31  end;