# HG changeset patch
# User wenzelm
# Date 949697010 -3600
# Node ID 626504b52668ca5742cd60b8558aa79a02605ca7
# Parent  f8a29f5a0433ae76bed608a30e7ac3e109f23c79
tuned;

diff -r f8a29f5a0433 -r 626504b52668 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Fri Feb 04 21:37:23 2000 +0100
+++ b/src/Pure/Thy/html.ML	Fri Feb 04 21:43:30 2000 +0100
@@ -28,7 +28,7 @@
   val applet_pages: string -> Url.T -> Url.T * string -> bool -> (string * string) list
   val theory_entry: Url.T * string -> text
   val session_entries: (Url.T * string) list -> text
-  val verbatim_source: string list -> text
+  val verbatim_source: Symbol.symbol list -> text
   val begin_theory: Url.T * string -> string -> (Url.T option * string) list ->
     (Url.T option * Url.T * bool option) list -> text -> text
   val end_theory: text