# HG changeset patch # User wenzelm # Date 1266789937 -3600 # Node ID 9927471cca354b234d77802c657c8d064d16d9fa # Parent 9ea4445d2ccf30a8f615ffbece5a26c407fd94ce filter out authentic const syntax; diff -r 9ea4445d2ccf -r 9927471cca35 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Sun Feb 21 22:35:02 2010 +0100 +++ b/src/Pure/Syntax/syntax.ML Sun Feb 21 23:05:37 2010 +0100 @@ -302,7 +302,7 @@ lexicon = if changed then fold Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon, gram = if changed then Parser.extend_gram gram xprods else gram, - consts = Library.merge (op =) (consts1, filter_out Long_Name.is_qualified consts2), + consts = Library.merge (op =) (consts1, filter_out (can Lexicon.unmark_const) consts2), prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)), parse_ast_trtab = update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,