# 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,