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