src/Pure/Syntax/syntax.ML
changeset 28840 049f0a8faa35
parent 28413 ee73353fb87c
child 28904 3ef9489eeef5
     1.1 --- a/src/Pure/Syntax/syntax.ML	Tue Nov 18 18:25:42 2008 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Nov 18 18:25:45 2008 +0100
     1.3 @@ -400,7 +400,7 @@
     1.4  local
     1.5  
     1.6  fun pretty_strs_qs name strs =
     1.7 -  Pretty.strs (name :: map Library.quote (sort_strings strs));
     1.8 +  Pretty.strs (name :: map quote (sort_strings strs));
     1.9  
    1.10  fun pretty_gram (Syntax (tabs, _)) =
    1.11    let
    1.12 @@ -420,7 +420,7 @@
    1.13      fun pretty_ruletab name tab =
    1.14        Pretty.big_list name (map Ast.pretty_rule (dest_ruletab tab));
    1.15  
    1.16 -    fun pretty_tokentr (mode, trs) = Pretty.strs (Library.quote mode ^ ":" :: map fst trs);
    1.17 +    fun pretty_tokentr (mode, trs) = Pretty.strs (quote mode ^ ":" :: map fst trs);
    1.18  
    1.19      val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab,
    1.20        print_ruletab, print_ast_trtab, tokentrtab, ...} = tabs;