1.1 --- a/src/Pure/Thy/thy_info.ML	Tue Aug 03 21:34:38 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Aug 03 22:28:43 2010 +0200
     1.3 @@ -116,7 +116,7 @@
     1.4  
     1.5  fun lookup_theory name =
     1.6    (case lookup_thy name of
     1.7 -    SOME (_, SOME thy) => SOME thy
     1.8 +    SOME (_, SOME theory) => SOME theory
     1.9    | _ => NONE);
    1.10  
    1.11  fun get_theory name =
    1.12 @@ -135,19 +135,19 @@
    1.13  
    1.14  (* remove theory *)
    1.15  
    1.16 -fun remove_thy name =
    1.17 +fun remove_thy name = CRITICAL (fn () =>
    1.18    if is_finished name then error (loader_msg "attempt to change finished theory" [name])
    1.19    else
    1.20      let
    1.21        val succs = thy_graph Graph.all_succs [name];
    1.22        val _ = priority (loader_msg "removing" succs);
    1.23 -      val _ = CRITICAL (fn () =>
    1.24 -        (List.app (perform Remove) succs; change_thys (Graph.del_nodes succs)));
    1.25 -    in () end;
    1.26 +      val _ = List.app (perform Remove) succs;
    1.27 +      val _ = change_thys (Graph.del_nodes succs);
    1.28 +    in () end);
    1.29  
    1.30 -fun kill_thy name =
    1.31 +fun kill_thy name = CRITICAL (fn () =>
    1.32    if known_thy name then remove_thy name
    1.33 -  else ();
    1.34 +  else ());
    1.35  
    1.36  
    1.37  (* scheduling loader tasks *)
    1.38 @@ -335,15 +335,14 @@
    1.39  fun register_thy theory =
    1.40    let
    1.41      val name = Context.theory_name theory;
    1.42 -    val _ = kill_thy name;
    1.43 -    val _ = priority ("Registering theory " ^ quote name);
    1.44 -
    1.45      val master = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
    1.46      val parents = map Context.theory_name (Theory.parents_of theory);
    1.47      val deps = make_deps master parents;
    1.48    in
    1.49      CRITICAL (fn () =>
    1.50 -     (map get_theory parents;
    1.51 +     (kill_thy name;
    1.52 +      priority ("Registering theory " ^ quote name);
    1.53 +      map get_theory parents;
    1.54        change_thys (new_entry name parents (SOME deps, SOME theory));
    1.55        perform Update name))
    1.56    end;