--- a/src/Pure/Thy/html.ML Tue Nov 18 18:25:42 2008 +0100
+++ b/src/Pure/Thy/html.ML Tue Nov 18 18:25:45 2008 +0100
@@ -232,7 +232,7 @@
(* common markup *)
-fun span s = ("<span class=" ^ Library.quote (XML.text s) ^ ">", "</span>");
+fun span s = ("<span class=" ^ quote (XML.text s) ^ ">", "</span>");
val _ = Markup.add_mode htmlN (fn (name, _) => span name);
@@ -255,7 +255,7 @@
(* misc *)
-fun href_name s txt = "<a href=" ^ Library.quote s ^ ">" ^ txt ^ "</a>";
+fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>";
fun href_path path txt = href_name (Url.implode path) txt;
fun href_opt_path NONE txt = txt