src/Tools/WWW_Find/find_theorems.ML

       |> the_default "Main";
     val with_dups = is_some (args "with_dups");
 
     fun do_find () =
       let
-        val ctxt = ProofContext.init (theory thy_name);
+        val ctxt = ProofContext.init_global (theory thy_name);
         val query = get_query ();
         val (othmslen, thms) = apsnd rev
           (Find_Theorems.find_theorems ctxt NONE (SOME limit) with_dups query);
         val thmslen = length thms;
         fun thm_row args = Xhtml.write send (html_thm ctxt args);