# HG changeset patch
# User wenzelm
# Date 963863079 -7200
# Node ID 63cca60b2ccebc32ec4e822b271949cdc607e4f3
# Parent  21cfeae6659d933aeb0bf40a1e2a534b1d8541a8
consts: include *all* names;

diff -r 21cfeae6659d -r 63cca60b2cce src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Mon Jul 17 18:17:54 2000 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Mon Jul 17 21:44:39 2000 +0200
@@ -311,7 +311,7 @@
     SynExt {
       logtypes = logtypes',
       xprods = xprods,
-      consts = filter Lexicon.is_xid (consts union mfix_consts),
+      consts = consts union mfix_consts,
       prmodes = distinct (map (fn (m, _, _) => m) tokentrfuns),
       parse_ast_translation = parse_ast_translation,
       parse_rules = parse_rules,