src/Pure/pure_thy.ML

     ("",            typ "id_position => logic",        Delimfix "_"),
     ("",            typ "longid_position => logic",    Delimfix "_"),
     ("",            typ "var => logic",                Delimfix "_"),
     ("_DDDOT",      typ "logic",                       Delimfix "..."),
     ("_strip_positions", typ "'a", NoSyn),
-    ("_constify",   typ "num => num_const",            Delimfix "_"),
+    ("_constify",   typ "num_token => num_const",      Delimfix "_"),
     ("_constify",   typ "float_token => float_const",  Delimfix "_"),
+    ("_constify",   typ "xnum_token => xnum_const",    Delimfix "_"),
     ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
     ("_indexdefault", typ "index",                     Delimfix ""),
     ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
     ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
     ("_update_name", typ "idt",                        NoSyn),
     ("_constrainAbs", typ "'a",                        NoSyn),
     ("_position",   typ "id => id_position",           Delimfix "_"),
     ("_position",   typ "longid => longid_position",   Delimfix "_"),
-    ("_position",   typ "xstr => xstr_position",   Delimfix "_"),
+    ("_position",   typ "xstr => xstr_position",       Delimfix "_"),
     ("_type_constraint_", typ "'a",                    NoSyn),
     ("_context_const", typ "id_position => logic",     Delimfix "CONST _"),
     ("_context_const", typ "id_position => aprop",     Delimfix "CONST _"),
     ("_context_const", typ "longid_position => logic", Delimfix "CONST _"),
     ("_context_const", typ "longid_position => aprop", Delimfix "CONST _"),