diff -r bfba1352239a -r 96ccc8972fc7 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sat Nov 16 21:29:18 2013 +0100
+++ b/src/Pure/Thy/present.ML	Sat Nov 16 22:17:45 2013 +0100
@@ -7,7 +7,6 @@
 signature PRESENT =
 sig
   val session_name: theory -> string
-  val no_document: ('a -> 'b) -> 'a -> 'b  (*not thread-safe!*)
   val read_variant: string -> string * string
   val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     string * string -> bool * string -> bool -> theory list -> unit  (*not thread-safe!*)
@@ -138,9 +137,6 @@
 fun change_browser_info f =
   CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f));
 
-val suppress_tex_source = Unsynchronized.ref false;
-fun no_document f x = Unsynchronized.setmp suppress_tex_source true f x;
-
 fun init_theory_info name info =
   change_browser_info (fn (theories, tex_index, html_index, graph) =>
     (Symtab.update (name, info) theories, tex_index, html_index, graph));
@@ -165,10 +161,6 @@
   change_browser_info (fn (theories, tex_index, html_index, graph) =>
     (theories, tex_index, html_index, ins_graph_entry entry graph));
 
-fun put_tex_source name tex_source =
-  if ! suppress_tex_source then ()
-  else change_theory_info name (fn (_, html_source) => (tex_source, html_source));
-
 
 
 (** global session state **)
@@ -380,7 +372,8 @@
 (* theory elements *)
 
 fun theory_output name s =
-  with_session_info () (fn _ => put_tex_source name (Latex.isabelle_file name s));
+  with_session_info () (fn _ =>
+    change_theory_info name (fn (_, html_source) => (Latex.isabelle_file name s, html_source)));
 
 fun begin_theory update_time mk_text thy =
   with_session_info thy (fn {name = session_name, chapter, ...} =>