changeset 28375 | c879d88d038a |
parent 27889 | c9e8a5bda32b |
child 28407 | f9db1da584ac |
--- a/src/Pure/Syntax/syntax.ML Fri Sep 26 17:24:15 2008 +0200 +++ b/src/Pure/Syntax/syntax.ML Fri Sep 26 19:07:56 2008 +0200 @@ -405,7 +405,7 @@ fun pretty_gram (Syntax (tabs, _)) = let val {lexicon, prmodes, gram, prtabs, ...} = tabs; - val prmodes' = sort_strings (filter_out (equal "") prmodes); + val prmodes' = sort_strings (filter_out (fn s => s = "") prmodes); in [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon), Pretty.big_list "prods:" (Parser.pretty_gram gram),