src/Pure/pure_thy.ML

     ("",            typ "pttrn => pttrns",             Delimfix "_"),
     ("_pttrns",     typ "pttrn => pttrns => pttrns",   Mixfix ("_/ _", [1, 0], 0)),
     ("",            typ "aprop => aprop",              Delimfix "'(_')"),
     ("",            typ "id_position => aprop",        Delimfix "_"),
     ("",            typ "longid_position => aprop",    Delimfix "_"),
-    ("",            typ "var => aprop",                Delimfix "_"),
+    ("",            typ "var_position => aprop",       Delimfix "_"),
     ("_DDDOT",      typ "aprop",                       Delimfix "..."),
     ("_aprop",      typ "aprop => prop",               Delimfix "PROP _"),
     ("_asm",        typ "prop => asms",                Delimfix "_"),
     ("_asms",       typ "prop => asms => asms",        Delimfix "_;/ _"),
     ("_bigimpl",    typ "asms => prop => prop",        Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
     ("_ofclass",    typ "type => logic => prop",       Delimfix "(1OFCLASS/(1'(_,/ _')))"),
     ("_mk_ofclass", typ "dummy",                       NoSyn),
     ("_TYPE",       typ "type => logic",               Delimfix "(1TYPE/(1'(_')))"),
     ("",            typ "id_position => logic",        Delimfix "_"),
     ("",            typ "longid_position => logic",    Delimfix "_"),
-    ("",            typ "var => logic",                Delimfix "_"),
+    ("",            typ "var_position => logic",       Delimfix "_"),
     ("_DDDOT",      typ "logic",                       Delimfix "..."),
     ("_strip_positions", typ "'a", NoSyn),
     ("_position",   typ "num_token => num_position",   Delimfix "_"),
     ("_position",   typ "float_token => float_position", Delimfix "_"),
     ("_position",   typ "xnum_token => xnum_position", Delimfix "_"),

     ("_constrainAbs", typ "'a",                        NoSyn),
     ("_position_sort", typ "tid => tid_position",      Delimfix "_"),
     ("_position_sort", typ "tvar => tvar_position",    Delimfix "_"),
     ("_position",   typ "id => id_position",           Delimfix "_"),
     ("_position",   typ "longid => longid_position",   Delimfix "_"),
+    ("_position",   typ "var => var_position",         Delimfix "_"),
     ("_position",   typ "str_token => str_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 _"),