Replaced quote by Library.quote, since quote now refers to Symbol.quote

--- a/src/HOL/thy_syntax.ML	Fri Apr 16 18:44:39 2004 +0200
+++ b/src/HOL/thy_syntax.ML	Fri Apr 16 18:45:56 2004 +0200
@@ -57,7 +57,7 @@
     fun mk_params ((recs, ipairs), monos) =
       let val big_rec_name = space_implode "_" (map (scan_to_id o unenclose) recs)
           and srec_tms = mk_list recs
-          and sintrs   = mk_big_list (no_atts (map (mk_pair o apfst quote) ipairs))
+          and sintrs   = mk_big_list (no_atts (map (mk_pair o apfst Library.quote) ipairs))
       in
         ";\n\n\
         \local\n\
@@ -133,7 +133,7 @@
       val names = map (fn ((((alt_name, _), name), _), _) =>
         unenclose (if_none alt_name name)) dts;
 
-      val add_datatype_args = brackets (commas (map quote names)) ^ " " ^
+      val add_datatype_args = brackets (commas (map Library.quote names)) ^ " " ^
         brackets (commas (map (fn ((((_, vs), name), mx), cs) =>
           parens (brackets (commas vs) ^ ", " ^ name ^ ", " ^ mx ^ ", " ^
             brackets (commas cs))) dts));
@@ -156,7 +156,7 @@
     \  case_thms, split_thms, induction, size, simps}) =\n\
     \ DatatypePackage.rep_datatype " ^
     (case names of
-        Some names => "(Some [" ^ commas_quote names ^ "])\n " ^
+        Some names => "(Some [" ^ Library.commas_quote names ^ "])\n " ^
           mk_thmss distinct ^ "\n " ^ mk_thmss inject ^
             "\n " ^ mk_thm induct ^ " thy;\nin\n" ^ mk_bind_thms_string names
       | None => "None\n " ^ mk_thmss distinct ^ "\n " ^ mk_thmss inject ^
@@ -179,7 +179,7 @@
   val opt_typs = repeat ((string >> unenclose) ||
     simple_typ || ("(" $$-- complex_typ --$$ ")"));
   val constructor = name -- opt_typs -- opt_mixfix >> (fn ((n, Ts), mx) =>
-    parens (n ^ ", " ^ brackets (commas_quote Ts) ^ ", " ^ mx));
+    parens (n ^ ", " ^ brackets (Library.commas_quote Ts) ^ ", " ^ mx));
   val opt_name = optional ("(" $$-- name --$$ ")" >> Some) None
 
   fun optlistlist s = optional (s $$-- enum "and" (list name)) [[]]
@@ -199,7 +199,7 @@
 (** primrec **)
 
 fun mk_patterns eqns = mk_list (map (fn (s, _) => if s = "" then "_" else s) eqns);
-fun mk_eqns eqns = mk_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) eqns);
+fun mk_eqns eqns = mk_list (map (fn (x, y) => mk_pair (mk_pair (Library.quote x, y), "[]")) eqns);
 
 fun mk_primrec_decl (alt_name, eqns) =
   ";\nval (thy, " ^ mk_patterns eqns ^ ") = PrimrecPackage.add_primrec " ^ alt_name ^ " "
@@ -221,7 +221,7 @@
     ";\n\n\
     \local\n\
     \fun simpset() = Simplifier.simpset_of thy;\n\
-    \val (thy, result) = thy |> RecdefPackage.add_recdef_old " ^ quote fid ^ " " ^ rel ^ "\n" ^
+    \val (thy, result) = thy |> RecdefPackage.add_recdef_old " ^ Library.quote fid ^ " " ^ rel ^ "\n" ^
     mk_eqns eqns ^ "\n(" ^ ss ^ ",\n " ^ mk_list congs ^ ");\n\
     \in\n\
     \structure " ^ fid ^ " =\n\
@@ -251,7 +251,7 @@
   in
     ";\n\n\
     \local\n\
-    \val (thy, result) = thy |> RecdefPackage.defer_recdef " ^ quote fid ^ "\n" ^
+    \val (thy, result) = thy |> RecdefPackage.defer_recdef " ^ Library.quote fid ^ "\n" ^
     axms_text ^ "\n" ^ congs_text ^ ";\n\
     \in\n\
     \structure " ^ fid ^ " =\n\

--- a/src/Pure/Isar/antiquote.ML	Fri Apr 16 18:44:39 2004 +0200
+++ b/src/Pure/Isar/antiquote.ML	Fri Apr 16 18:45:56 2004 +0200
@@ -44,7 +44,7 @@
   | escape "\"" = "\\\""
   | escape s = s;
 
-val quote_escape = quote o implode o map escape o Symbol.explode;
+val quote_escape = Library.quote o implode o map escape o Symbol.explode;
 
 val scan_ant =
   T.scan_blank ||

--- a/src/Pure/Isar/isar_thy.ML	Fri Apr 16 18:44:39 2004 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Fri Apr 16 18:45:56 2004 +0200
@@ -565,7 +565,7 @@
     \val thms = PureThy.get_thms_closure (Context.the_context ());\n\
     \val method: bstring * (Args.src -> Proof.context -> Proof.method) * string"
     "PureIsar.Method.add_method method"
-    ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")");
+    ("(" ^ Library.quote name ^ ", " ^ txt ^ ", " ^ Library.quote cmt ^ ")");
 
 
 (* add_oracle *)
@@ -574,7 +574,7 @@
   Context.use_let
     "val oracle: bstring * (Sign.sg * Object.T -> term)"
     "Theory.add_oracle oracle"
-    ("(" ^ quote name ^ ", " ^ txt ^ ")");
+    ("(" ^ Library.quote name ^ ", " ^ txt ^ ")");
 
 
 (* add_locale *)

--- a/src/Pure/Syntax/syntax.ML	Fri Apr 16 18:44:39 2004 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Apr 16 18:45:56 2004 +0200
@@ -264,7 +264,7 @@
 (** inspect syntax **)
 
 fun pretty_strs_qs name strs =
-  Pretty.strs (name :: map quote (sort_strings strs));
+  Pretty.strs (name :: map Library.quote (sort_strings strs));
 
 
 (* print_gram *)
@@ -292,7 +292,7 @@
     fun pretty_ruletab name tab =
       Pretty.big_list name (map Ast.pretty_rule (dest_ruletab tab));
 
-    fun pretty_tokentr (mode, trs) = Pretty.strs (quote mode ^ ":" :: map fst trs);
+    fun pretty_tokentr (mode, trs) = Pretty.strs (Library.quote mode ^ ":" :: map fst trs);
 
     val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab,
       print_ruletab, print_ast_trtab, tokentrtab, ...} = tabs;

--- 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

--- a/src/Pure/Thy/latex.ML	Fri Apr 16 18:44:39 2004 +0200
+++ b/src/Pure/Thy/latex.ML	Fri Apr 16 18:45:56 2004 +0200
@@ -102,7 +102,7 @@
           "\\isacommand{" ^ output_syms s ^ "}"
         else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then
           "\\isakeyword{" ^ output_syms s ^ "}"
-        else if T.is_kind T.String tok then output_syms (quote s)
+        else if T.is_kind T.String tok then output_syms (Library.quote s)
         else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
         else output_syms s
       end

--- a/src/Pure/Thy/present.ML	Fri Apr 16 18:44:39 2004 +0200
+++ b/src/Pure/Thy/present.ML	Fri Apr 16 18:45:56 2004 +0200
@@ -100,7 +100,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 quote parents) ^ " ;") gr));
+    path ^ "\" > " ^ space_implode " " (map Library.quote parents) ^ " ;") gr));
 
 fun ID_of sess s = space_implode "/" (sess @ [s]);
 

--- a/src/Pure/Thy/thy_parse.ML	Fri Apr 16 18:44:39 2004 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Fri Apr 16 18:45:56 2004 +0200
@@ -138,7 +138,7 @@
 val ident = kind Ident;
 val long_ident = kind LongIdent;
 val long_id = ident || long_ident;
-val type_var = kind TypeVar >> quote;
+val type_var = kind TypeVar >> Library.quote;
 val nat = kind Nat;
 val string = kind String;
 val verbatim = kind Verbatim;
@@ -181,7 +181,7 @@
 
 (* names *)
 
-val name = ident >> quote || string;
+val name = ident >> Library.quote || string;
 val names = list name;
 val names1 = list1 name;
 val name_list = names >> mk_list;
@@ -202,7 +202,7 @@
 
 (* arities *)
 
-val sort = name || "{" $$-- list ident --$$ "}" >> (quote o enclose "{" "}" o commas);
+val sort = name || "{" $$-- list ident --$$ "}" >> (Library.quote o enclose "{" "}" o commas);
 val sort_list1 = list1 sort >> mk_list;
 
 val arity = optional ("(" $$-- !! (sort_list1 --$$")")) "[]" -- sort;
@@ -273,7 +273,7 @@
       "(" $$-- const_type true --$$ ")" >> parens) toks
   end;
 
-val typ = string || (const_type false >> quote);
+val typ = string || (const_type false >> Library.quote);
 
 
 fun mk_old_type_decl ((ts, n), syn) =
@@ -352,8 +352,8 @@
 
 (* axioms *)
 
-val mk_axms = mk_big_list o map (mk_pair o apfst quote);
-val mk_axms' = mk_big_list o map (mk_pair o rpair "[]" o mk_pair o apfst quote);
+val mk_axms = mk_big_list o map (mk_pair o apfst Library.quote);
+val mk_axms' = mk_big_list o map (mk_pair o rpair "[]" o mk_pair o apfst Library.quote);
 
 fun mk_axiom_decls axms = (mk_axms axms, map fst axms);
 
@@ -371,7 +371,7 @@
   let
     val (axms_defs, axms_names) =
       mk_axiom_decls (map (fn ((id, _), def) => (id ^ "_def", def)) x);
-  in ((mk_big_list o map mk_triple2 o map (apfst quote o fst)) x ^
+  in ((mk_big_list o map mk_triple2 o map (apfst Library.quote o fst)) x ^
        "\n\n|> (#1 oo (PureThy.add_defs false o map Thm.no_attributes))\n" ^ axms_defs, axms_names)
   end;
 
@@ -416,16 +416,16 @@
 
 val locale_decl =
   (name --$$ "=") -- 
-    (optional ((ident >> (fn x => parens ("Some" ^ quote x))) --$$ "+") ("None")) --
+    (optional ((ident >> (fn x => parens ("Some" ^ Library.quote x))) --$$ "+") ("None")) --
     ("fixes" $$--
       (repeat (name --$$ "::" -- !! (typ -- opt_mixfix)) 
        >> (mk_big_list o map mk_triple2))) --
     (optional 
-     ("assumes" $$-- (repeat ((ident >> quote) -- !! string) 
+     ("assumes" $$-- (repeat ((ident >> Library.quote) -- !! string) 
 		     >> (mk_list o map mk_pair)))
      "[]") --
     (optional 
-     ("defines" $$-- (repeat ((ident >> quote) -- !! string) 
+     ("defines" $$-- (repeat ((ident >> Library.quote) -- !! string) 
 		      >> (mk_list o map mk_pair)))
      "[]")
   >> (fn ((((nm, ext), cs), asms), defs) => cat_lines [nm, ext, cs, asms, defs]);
@@ -454,7 +454,7 @@
 (* header *)
 
 fun mk_header (thy_name, parents) =
-  (thy_name, "IsarThy.begin_theory " ^ cat (quote thy_name) (mk_list parents) ^ " []");
+  (thy_name, "IsarThy.begin_theory " ^ cat (Library.quote thy_name) (mk_list parents) ^ " []");
 
 val header = ident --$$ "=" -- enum1 "+" name >> mk_header;
 
@@ -524,7 +524,7 @@
 
 (* standard sections *)
 
-fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy " ^ quote ax ^ ";";
+fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy " ^ Library.quote ax ^ ";";
 val mk_vals = cat_lines o map mk_val;
 
 fun mk_axm_sect "" (txt, axs) = (txt, mk_vals axs)

--- a/src/Pure/codegen.ML	Fri Apr 16 18:44:39 2004 +0200
+++ b/src/Pure/codegen.ML	Fri Apr 16 18:45:56 2004 +0200
@@ -491,7 +491,8 @@
 fun output_code gr xs = implode (map (snd o Graph.get_node gr)
   (rev (Graph.all_preds gr xs)));
 
-fun gen_generate_code prep_term thy = Pretty.setmp_margin (!margin) (fn xs =>
+fun gen_generate_code prep_term thy =
+  setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs =>
   let
     val sg = sign_of thy;
     val gr = Graph.new_node ("<Top>", (None, "")) Graph.empty;
@@ -504,7 +505,7 @@
     space_implode "\n\n" (map (fn (s', p) => Pretty.string_of (Pretty.block
       [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"])) ps) ^
     "\n\nend;\n\nopen Generated;\n"
-  end);
+  end));
 
 val generate_code_i = gen_generate_code (K I);
 val generate_code = gen_generate_code
@@ -574,7 +575,7 @@
               Pretty.block [Pretty.str "Library.Some ", Pretty.block (Pretty.str "[" ::
                 flat (separate [Pretty.str ",", Pretty.brk 1]
                   (map (fn (s, T) => [Pretty.block
-                    [Pretty.str ("(" ^ quote s ^ ","), Pretty.brk 1,
+                    [Pretty.str ("(" ^ Library.quote s ^ ","), Pretty.brk 1,
                      mk_app false (mk_term_of sg false T)
                        [Pretty.str s], Pretty.str ")"]]) frees)) @
                   [Pretty.str "]"])]],

--- a/src/Pure/display.ML	Fri Apr 16 18:44:39 2004 +0200
+++ b/src/Pure/display.ML	Fri Apr 16 18:45:56 2004 +0200
@@ -64,7 +64,7 @@
 val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
 val show_tags = ref false;      (*false: suppress tags*)
 
-fun pretty_tag (name, args) = Pretty.strs (name :: map quote args);
+fun pretty_tag (name, args) = Pretty.strs (name :: map Library.quote args);
 val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
 
 fun pretty_flexpair pretty_term (t, u) = Pretty.block
@@ -166,8 +166,8 @@
 fun pretty_name_space (kind, space) =
   let
     fun prt_entry (name, accs) = Pretty.block
-      (Pretty.str (quote name ^ " =") :: Pretty.brk 1 ::
-        Pretty.commas (map (Pretty.str o quote) accs));
+      (Pretty.str (Library.quote name ^ " =") :: Pretty.brk 1 ::
+        Pretty.commas (map (Pretty.quote o Pretty.str) accs));
   in
     Pretty.fbreaks (Pretty.str (kind ^ ":") :: map prt_entry (NameSpace.dest space))
     |> Pretty.block

--- a/src/ZF/thy_syntax.ML	Fri Apr 16 18:44:39 2004 +0200
+++ b/src/ZF/thy_syntax.ML	Fri Apr 16 18:45:56 2004 +0200
@@ -43,7 +43,7 @@
                            (map (scan_to_id o unenclose) recs)
           and srec_tms = mk_list recs
           and sintrs   =
-            mk_big_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) ipairs)
+            mk_big_list (map (fn (x, y) => mk_pair (mk_pair (Library.quote x, y), "[]")) ipairs)
           and inames   = mk_list (map (mk_bind "" o fst) ipairs)
       in
          ";\n\n\
@@ -155,7 +155,7 @@
 fun mk_primrec_decl eqns =
   let val binds = map (mk_bind "" o fst) eqns in
     ";\nval (thy, " ^ mk_list binds ^ ") = PrimrecPackage.add_primrec " ^
-      mk_list (map (fn p => mk_pair (mk_pair p, "[]")) (map (apfst quote) eqns)) ^ " " ^ " thy;\n\
+      mk_list (map (fn p => mk_pair (mk_pair p, "[]")) (map (apfst Library.quote) eqns)) ^ " " ^ " thy;\n\
     \val thy = thy\n"
   end;