1.1 --- a/src/Pure/Thy/thy_info.ML	Wed Aug 04 15:14:48 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Aug 04 15:45:49 2010 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4  local
     1.5    val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list);
     1.6  in
     1.7 -  fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
     1.8 +  fun add_hook f = NAMED_CRITICAL "Thy_Info" (fn () => Unsynchronized.change hooks (cons f));
     1.9    fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks);
    1.10  end;
    1.11  
    1.12 @@ -75,7 +75,7 @@
    1.13    val database = Unsynchronized.ref (Graph.empty: (deps option * theory option) Graph.T);
    1.14  in
    1.15    fun get_thys () = ! database;
    1.16 -  fun change_thys f = CRITICAL (fn () => Unsynchronized.change database f);
    1.17 +  fun change_thys f = NAMED_CRITICAL "Thy_Info" (fn () => Unsynchronized.change database f);
    1.18  end;
    1.19  
    1.20  
    1.21 @@ -124,10 +124,10 @@
    1.22      SOME theory => theory
    1.23    | _ => error (loader_msg "undefined theory entry for" [name]));
    1.24  
    1.25 -fun loaded_files name =
    1.26 +fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () =>
    1.27    (case get_deps name of
    1.28      NONE => []
    1.29 -  | SOME {master = (thy_path, _), ...} => thy_path :: Thy_Load.loaded_files (get_theory name));
    1.30 +  | SOME {master = (thy_path, _), ...} => thy_path :: Thy_Load.loaded_files (get_theory name)));
    1.31  
    1.32  
    1.33  
    1.34 @@ -135,7 +135,7 @@
    1.35  
    1.36  (* remove theory *)
    1.37  
    1.38 -fun remove_thy name = CRITICAL (fn () =>
    1.39 +fun remove_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>
    1.40    if is_finished name then error (loader_msg "attempt to change finished theory" [name])
    1.41    else
    1.42      let
    1.43 @@ -145,7 +145,7 @@
    1.44        val _ = change_thys (Graph.del_nodes succs);
    1.45      in () end);
    1.46  
    1.47 -fun kill_thy name = CRITICAL (fn () =>
    1.48 +fun kill_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>
    1.49    if known_thy name then remove_thy name
    1.50    else ());
    1.51  
    1.52 @@ -236,7 +236,7 @@
    1.53      val parent_names = map Context.theory_name parent_thys;
    1.54      fun after_load' () =
    1.55       (after_load ();
    1.56 -      CRITICAL (fn () =>
    1.57 +      NAMED_CRITICAL "Thy_Info" (fn () =>
    1.58          (change_thys (new_entry name parent_names (SOME deps, SOME theory));
    1.59            perform Update name)));
    1.60  
    1.61 @@ -333,7 +333,7 @@
    1.62      val parents = map Context.theory_name (Theory.parents_of theory);
    1.63      val deps = make_deps master parents;
    1.64    in
    1.65 -    CRITICAL (fn () =>
    1.66 +    NAMED_CRITICAL "Thy_Info" (fn () =>
    1.67       (kill_thy name;
    1.68        priority ("Registering theory " ^ quote name);
    1.69        map get_theory parents;