src/Pure/Syntax/syntax.ML

 (** print syntax **)
 
 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
     val {lexicon, prmodes, gram, prtabs, ...} = tabs;
     val prmodes' = sort_strings (filter_out (fn s => s = "") prmodes);

       pretty_strs_qs name (Symtab.keys tab);
 
     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;
   in
     [pretty_strs_qs "consts:" consts,