diff -r 1d977436c1bf -r f4b1440d9880 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Sat Nov 16 20:20:09 2013 +0100
+++ b/src/Pure/Thy/html.ML	Sat Nov 16 21:18:31 2013 +0100
@@ -23,8 +23,7 @@
   val begin_session_index: string -> (Url.T * string) list -> Url.T -> text
   val applet_pages: string -> Url.T * string -> (string * string) list
   val theory_entry: Url.T * string -> text
-  val theory_source: text -> text
-  val begin_theory: string -> (Url.T option * string) list -> text -> text
+  val theory: string -> (Url.T option * string) list -> text -> text
 end;
 
 structure HTML: HTML =
@@ -320,13 +319,12 @@
 
 (* theory *)
 
-val theory_source = enclose
-  "\n</div>\n<div class=\"source\">\n<pre>"
-  "</pre>\n";
-
-fun begin_theory A Bs body =
-  begin_document ("Theory " ^ A) ^ "\n" ^ command "theory" ^ " " ^ name A ^ "<br/>\n" ^
+fun theory A Bs txt =
+  begin_document ("Theory " ^ A) ^ "\n" ^
+  command "theory" ^ " " ^ name A ^ "<br/>\n" ^
   keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs) ^
-  "<br/>\n" ^ body;
+  "<br/>\n" ^
+  enclose "\n</div>\n<div class=\"source\">\n<pre>" "</pre>\n" txt ^
+  end_document;
 
 end;