src/Pure/pure_thy.ML
changeset 51612 6a1e40f9dd55
parent 50636 07f47142378e
child 52143 36ffe23b25f8
     1.1 --- a/src/Pure/pure_thy.ML	Thu Apr 04 10:30:28 2013 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Thu Apr 04 12:06:23 2013 +0200
     1.3 @@ -111,7 +111,7 @@
     1.4      ("",            typ "aprop => aprop",              Delimfix "'(_')"),
     1.5      ("",            typ "id_position => aprop",        Delimfix "_"),
     1.6      ("",            typ "longid_position => aprop",    Delimfix "_"),
     1.7 -    ("",            typ "var => aprop",                Delimfix "_"),
     1.8 +    ("",            typ "var_position => aprop",       Delimfix "_"),
     1.9      ("_DDDOT",      typ "aprop",                       Delimfix "..."),
    1.10      ("_aprop",      typ "aprop => prop",               Delimfix "PROP _"),
    1.11      ("_asm",        typ "prop => asms",                Delimfix "_"),
    1.12 @@ -122,7 +122,7 @@
    1.13      ("_TYPE",       typ "type => logic",               Delimfix "(1TYPE/(1'(_')))"),
    1.14      ("",            typ "id_position => logic",        Delimfix "_"),
    1.15      ("",            typ "longid_position => logic",    Delimfix "_"),
    1.16 -    ("",            typ "var => logic",                Delimfix "_"),
    1.17 +    ("",            typ "var_position => logic",       Delimfix "_"),
    1.18      ("_DDDOT",      typ "logic",                       Delimfix "..."),
    1.19      ("_strip_positions", typ "'a", NoSyn),
    1.20      ("_position",   typ "num_token => num_position",   Delimfix "_"),
    1.21 @@ -141,6 +141,7 @@
    1.22      ("_position_sort", typ "tvar => tvar_position",    Delimfix "_"),
    1.23      ("_position",   typ "id => id_position",           Delimfix "_"),
    1.24      ("_position",   typ "longid => longid_position",   Delimfix "_"),
    1.25 +    ("_position",   typ "var => var_position",         Delimfix "_"),
    1.26      ("_position",   typ "str_token => str_position",   Delimfix "_"),
    1.27      ("_type_constraint_", typ "'a",                    NoSyn),
    1.28      ("_context_const", typ "id_position => logic",     Delimfix "CONST _"),