filter out authentic const syntax;
authorwenzelm
Sun, 21 Feb 2010 23:05:37 +0100
changeset 35263 9927471cca35
parent 35262 9ea4445d2ccf
child 35275 3745987488b2
filter out authentic const syntax;
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,