src/Pure/Thy/thy_info.ML
changeset 25994 d35484265f46
parent 25775 90525e67ede7
child 26415 1b624d6e9163
     1.1 --- a/src/Pure/Thy/thy_info.ML	Sun Jan 27 22:21:35 2008 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Sun Jan 27 22:21:37 2008 +0100
     1.3 @@ -485,8 +485,7 @@
     1.4  fun gen_use_thy req str =
     1.5    let val name = base_name str in
     1.6      check_unfinished warning name;
     1.7 -    gen_use_thy' req Path.current str;
     1.8 -    CRITICAL (fn () => ML_Context.set_context (SOME (Context.Theory (get_theory name))))
     1.9 +    gen_use_thy' req Path.current str
    1.10    end;
    1.11  
    1.12  in
    1.13 @@ -532,9 +531,6 @@
    1.14      val dir = master_dir'' (lookup_deps name);
    1.15      val _ = check_unfinished error name;
    1.16      val _ = if int then use_thys_dir dir parents else ();
    1.17 -    (* FIXME tmp *)
    1.18 -    val _ = CRITICAL (fn () =>
    1.19 -      ML_Context.set_context (SOME (Context.Theory (get_theory (List.last parent_names)))));
    1.20  
    1.21      val theory = Theory.begin_theory name (map get_theory parent_names);
    1.22