# HG changeset patch
# User wenzelm
# Date 1227029145 -3600
# Node ID 049f0a8faa3564e2c1979fd9a97b7f9d1fd0eb4d
# Parent  32d498cf75956e2c65303a73b98d86a0b4900efc
tuned;

diff -r 32d498cf7595 -r 049f0a8faa35 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Nov 18 18:25:42 2008 +0100
+++ b/src/Pure/Syntax/syntax.ML	Tue Nov 18 18:25:45 2008 +0100
@@ -400,7 +400,7 @@
 local
 
 fun pretty_strs_qs name strs =
-  Pretty.strs (name :: map Library.quote (sort_strings strs));
+  Pretty.strs (name :: map quote (sort_strings strs));
 
 fun pretty_gram (Syntax (tabs, _)) =
   let
@@ -420,7 +420,7 @@
     fun pretty_ruletab name tab =
       Pretty.big_list name (map Ast.pretty_rule (dest_ruletab tab));
 
-    fun pretty_tokentr (mode, trs) = Pretty.strs (Library.quote mode ^ ":" :: map fst trs);
+    fun pretty_tokentr (mode, trs) = Pretty.strs (quote mode ^ ":" :: map fst trs);
 
     val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab,
       print_ruletab, print_ast_trtab, tokentrtab, ...} = tabs;
diff -r 32d498cf7595 -r 049f0a8faa35 src/Pure/Thy/html.ML
--- 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
diff -r 32d498cf7595 -r 049f0a8faa35 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Nov 18 18:25:42 2008 +0100
+++ b/src/Pure/Thy/present.ML	Tue Nov 18 18:25:45 2008 +0100
@@ -89,7 +89,7 @@
 fun write_graph gr path =
   File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
     "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
-    path ^ "\" > " ^ space_implode " " (map Library.quote parents) ^ " ;") gr));
+    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
 
 fun display_graph gr =
   let
diff -r 32d498cf7595 -r 049f0a8faa35 src/Pure/display.ML
--- a/src/Pure/display.ML	Tue Nov 18 18:25:42 2008 +0100
+++ b/src/Pure/display.ML	Tue Nov 18 18:25:45 2008 +0100
@@ -52,7 +52,7 @@
 val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
 val show_tags = ref false;      (*false: suppress tags*)
 
-fun pretty_tag (name, arg) = Pretty.strs [name, Library.quote arg];
+fun pretty_tag (name, arg) = Pretty.strs [name, quote arg];
 val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
 
 fun pretty_flexpair pp (t, u) = Pretty.block