src/Pure/Syntax/syntax.ML
changeset 35263 9927471cca35
parent 35130 0991c84e8dcf
child 35394 11f58c600707
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sun Feb 21 22:35:02 2010 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Feb 21 23:05:37 2010 +0100
     1.3 @@ -302,7 +302,7 @@
     1.4        lexicon =
     1.5          if changed then fold Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon,
     1.6        gram = if changed then Parser.extend_gram gram xprods else gram,
     1.7 -      consts = Library.merge (op =) (consts1, filter_out Long_Name.is_qualified consts2),
     1.8 +      consts = Library.merge (op =) (consts1, filter_out (can Lexicon.unmark_const) consts2),
     1.9        prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
    1.10        parse_ast_trtab =
    1.11          update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,