--- a/src/Pure/pure_thy.ML Fri Apr 08 20:39:09 2011 +0200
+++ b/src/Pure/pure_thy.ML Fri Apr 08 21:03:20 2011 +0200
@@ -137,14 +137,14 @@
("_constrain_position", typ "id => id_position", Delimfix "_"),
("_constrain_position", typ "longid => longid_position", Delimfix "_"),
("_type_constraint_", typ "'a", NoSyn),
- ("_context_const", typ "id => logic", Delimfix "CONST _"),
- ("_context_const", typ "id => aprop", Delimfix "CONST _"),
- ("_context_const", typ "longid => logic", Delimfix "CONST _"),
- ("_context_const", typ "longid => aprop", Delimfix "CONST _"),
- ("_context_xconst", typ "id => logic", Delimfix "XCONST _"),
- ("_context_xconst", typ "id => aprop", Delimfix "XCONST _"),
- ("_context_xconst", typ "longid => logic", Delimfix "XCONST _"),
- ("_context_xconst", typ "longid => aprop", Delimfix "XCONST _"),
+ ("_context_const", typ "id_position => logic", Delimfix "CONST _"),
+ ("_context_const", typ "id_position => aprop", Delimfix "CONST _"),
+ ("_context_const", typ "longid_position => logic", Delimfix "CONST _"),
+ ("_context_const", typ "longid_position => aprop", Delimfix "CONST _"),
+ ("_context_xconst", typ "id_position => logic", Delimfix "XCONST _"),
+ ("_context_xconst", typ "id_position => aprop", Delimfix "XCONST _"),
+ ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
+ ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
(const "==>", typ "prop => prop => prop", Delimfix "op ==>"),
(const Term.dummy_patternN, typ "aprop", Delimfix "'_"),
("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),