src/Pure/pure_thy.ML
changeset 46236 ae79f2978a67
parent 45703 c7a13ce60161
child 46483 10a9c31a22b4
     1.1 --- a/src/Pure/pure_thy.ML	Mon Jan 16 20:32:33 2012 +0100
     1.2 +++ b/src/Pure/pure_thy.ML	Mon Jan 16 21:50:15 2012 +0100
     1.3 @@ -125,9 +125,12 @@
     1.4      ("",            typ "var => logic",                Delimfix "_"),
     1.5      ("_DDDOT",      typ "logic",                       Delimfix "..."),
     1.6      ("_strip_positions", typ "'a", NoSyn),
     1.7 -    ("_constify",   typ "num_token => num_const",      Delimfix "_"),
     1.8 -    ("_constify",   typ "float_token => float_const",  Delimfix "_"),
     1.9 -    ("_constify",   typ "xnum_token => xnum_const",    Delimfix "_"),
    1.10 +    ("_position",   typ "num_token => num_position",   Delimfix "_"),
    1.11 +    ("_position",   typ "float_token => float_position", Delimfix "_"),
    1.12 +    ("_position",   typ "xnum_token => xnum_position", Delimfix "_"),
    1.13 +    ("_constify",   typ "num_position => num_const",   Delimfix "_"),
    1.14 +    ("_constify",   typ "float_position => float_const", Delimfix "_"),
    1.15 +    ("_constify",   typ "xnum_position => xnum_const", Delimfix "_"),
    1.16      ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
    1.17      ("_indexdefault", typ "index",                     Delimfix ""),
    1.18      ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),