src/Pure/Thy/thy_info.ML

         " on file: " ^ quote (Path.implode path));
       SOME (make_deps present outdated master (AList.update (op =) (path, SOME info) files)))
   | provide _ _ _ NONE = NONE;
 
 fun run_file path =
-  (case Option.map Context.theory_name (Context.get_context ()) of
+  (case Option.map (Context.theory_name o Context.the_theory) (Context.get_context ()) of
     NONE => (ThyLoad.load_file NONE path; ())
   | SOME name => (case lookup_deps name of
       SOME deps => change_deps name (provide path name
         (ThyLoad.load_file (opt_path' deps) path))
     | NONE => (ThyLoad.load_file NONE path; ())));

       in (visited', (result, name)) end
   end;
 
 fun gen_use_thy' req prfx s = Output.toplevel_errors (fn () =>
   let val (_, (_, name)) = req [] prfx ([], s)
-  in Context.context (get_theory name) end) ();
+  in Context.set_context (SOME (Context.Theory (get_theory name))) end) ();
 
 fun gen_use_thy req = gen_use_thy' req Path.current;
 
 fun warn_finished f name = (check_unfinished warning name; f name);
 

     val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
 
     val _ = change_thys (update_node name bparents (deps, SOME (Theory.copy theory)));
     val theory' = theory |> present dir' name bparents uses;
     val _ = put_theory name (Theory.copy theory');
-    val ((), theory'') = Context.pass_theory theory' (List.app (load_file false)) uses_now;
+    val ((), theory'') =
+      Context.pass_context (Context.Theory theory') (List.app (load_file false)) uses_now
+      ||> Context.the_theory;
     val _ = put_theory name (Theory.copy theory'');
   in theory'' end;
 
 fun end_theory theory =
   let