src/Pure/pure_thy.ML
changeset 45703 c7a13ce60161
parent 45490 20c8c0cca555
child 46236 ae79f2978a67
     1.1 --- a/src/Pure/pure_thy.ML	Thu Dec 01 11:54:39 2011 +0100
     1.2 +++ b/src/Pure/pure_thy.ML	Thu Dec 01 12:25:27 2011 +0100
     1.3 @@ -125,8 +125,9 @@
     1.4      ("",            typ "var => logic",                Delimfix "_"),
     1.5      ("_DDDOT",      typ "logic",                       Delimfix "..."),
     1.6      ("_strip_positions", typ "'a", NoSyn),
     1.7 -    ("_constify",   typ "num => num_const",            Delimfix "_"),
     1.8 +    ("_constify",   typ "num_token => num_const",      Delimfix "_"),
     1.9      ("_constify",   typ "float_token => float_const",  Delimfix "_"),
    1.10 +    ("_constify",   typ "xnum_token => xnum_const",    Delimfix "_"),
    1.11      ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
    1.12      ("_indexdefault", typ "index",                     Delimfix ""),
    1.13      ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
    1.14 @@ -135,7 +136,7 @@
    1.15      ("_constrainAbs", typ "'a",                        NoSyn),
    1.16      ("_position",   typ "id => id_position",           Delimfix "_"),
    1.17      ("_position",   typ "longid => longid_position",   Delimfix "_"),
    1.18 -    ("_position",   typ "xstr => xstr_position",   Delimfix "_"),
    1.19 +    ("_position",   typ "xstr => xstr_position",       Delimfix "_"),
    1.20      ("_type_constraint_", typ "'a",                    NoSyn),
    1.21      ("_context_const", typ "id_position => logic",     Delimfix "CONST _"),
    1.22      ("_context_const", typ "id_position => aprop",     Delimfix "CONST _"),