--- a/src/Pure/Thy/html.ML Fri Apr 16 18:44:39 2004 +0200
+++ b/src/Pure/Thy/html.ML Fri Apr 16 18:45:56 2004 +0200
@@ -244,7 +244,7 @@
(* token translations *)
fun style stl =
- apfst (enclose ("<span class=" ^ quote stl ^ ">") "</span>") o output_width;
+ apfst (enclose ("<span class=" ^ Library.quote stl ^ ">") "</span>") o output_width;
val html_trans =
[("class", style "tclass"),
@@ -273,7 +273,7 @@
(* misc *)
-fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>";
+fun href_name s txt = "<a href=" ^ Library.quote s ^ ">" ^ txt ^ "</a>";
fun href_path path txt = href_name (Url.pack path) txt;
fun href_opt_name None txt = txt