src/Pure/Thy/thy_info.ML

   val master_directory: string -> Path.T
   val remove_thy: string -> unit
   type context =
     {options: Options.T,
      symbols: HTML.symbols,
-     bibtex_entries: string list,
      last_timing: Toplevel.transition -> Time.time}
   val use_theories: context -> string -> Path.T -> (string * Position.T) list -> unit
   val use_thy: string -> unit
   val script_thy: Position.T -> string -> theory -> theory
   val register_thy: theory -> unit

 (* context *)
 
 type context =
   {options: Options.T,
    symbols: HTML.symbols,
-   bibtex_entries: string list,
    last_timing: Toplevel.transition -> Time.time};
 
 fun default_context (): context =
   {options = Options.default (),
    symbols = HTML.no_symbols,
-   bibtex_entries = [],
    last_timing = K Time.zeroTime};
 
 
 (* scheduling loader tasks *)
 

     val thy = Toplevel.end_theory end_pos end_state;
   in (results, thy) end;
 
 fun eval_thy (context: context) update_time master_dir header text_pos text parents =
   let
-    val {options, symbols, bibtex_entries, last_timing} = context;
+    val {options, symbols, last_timing} = context;
     val (name, _) = #name header;
     val keywords =
       fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
         (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
 
     val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text);
     val elements = Thy_Element.parse_elements keywords spans;
 
     fun init () =
       Resources.begin_theory master_dir header parents
-      |> Present.begin_theory bibtex_entries update_time
+      |> Present.begin_theory update_time
         (fn () => implode (map (HTML.present_span symbols keywords) spans));
 
     val (results, thy) =
       cond_timeit true ("theory " ^ quote name)
         (fn () => excursion keywords master_dir last_timing init elements);