src/Pure/pure_thy.ML
changeset 42410 16bc5564535f
parent 42375 774df7c59508
child 44433 9fbee4aab115
     1.1 --- a/src/Pure/pure_thy.ML	Tue Apr 19 22:08:42 2011 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Tue Apr 19 22:32:49 2011 +0200
     1.3 @@ -134,8 +134,8 @@
     1.4      ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
     1.5      ("_update_name", typ "idt",                        NoSyn),
     1.6      ("_constrainAbs", typ "'a",                        NoSyn),
     1.7 -    ("_constrain_position", typ "id => id_position",   Delimfix "_"),
     1.8 -    ("_constrain_position", typ "longid => longid_position", Delimfix "_"),
     1.9 +    ("_position",   typ "id => id_position",           Delimfix "_"),
    1.10 +    ("_position",   typ "longid => longid_position",   Delimfix "_"),
    1.11      ("_type_constraint_", typ "'a",                    NoSyn),
    1.12      ("_context_const", typ "id_position => logic",     Delimfix "CONST _"),
    1.13      ("_context_const", typ "id_position => aprop",     Delimfix "CONST _"),