diff -r 16ed9b97c72d -r b3c665940d62 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Fri Oct 09 16:29:18 2015 +0200
+++ b/src/Pure/Thy/html.ML	Fri Oct 09 16:58:24 2015 +0200
@@ -16,8 +16,6 @@
   val href_path: Url.T -> text -> text
   val href_opt_path: Url.T option -> text -> text
   val para: text -> text
-  val preform: text -> text
-  val verbatim: string -> text
   val begin_document: string -> text
   val end_document: text
   val begin_session_index: string -> Url.T -> (Url.T * string) list -> text
@@ -253,8 +251,6 @@
   | href_opt_path (SOME p) txt = href_path p txt;
 
 fun para txt = "\n<p>" ^ txt ^ "</p>\n";
-fun preform txt = "<pre>" ^ txt ^ "</pre>";
-val verbatim = preform o output;
 
 
 (* document *)
@@ -295,7 +291,7 @@
   command "theory" ^ " " ^ name A ^ "<br/>\n" ^
   keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs) ^
   "<br/>\n" ^
-  enclose "\n</div>\n<div class=\"source\">\n<pre>" "</pre>\n" txt ^
+  enclose "\n</div>\n<div class=\"source\">\n<pre class=\"source\">" "</pre>\n" txt ^
   end_document;
 
 end;