--- a/src/Pure/pure_thy.ML Fri Apr 08 18:08:13 2011 +0200
+++ b/src/Pure/pure_thy.ML Fri Apr 08 20:39:09 2011 +0200
@@ -133,10 +133,18 @@
("_indexvar", typ "index", Delimfix "'\\<index>"),
("_struct", typ "index => logic", Mixfix ("\\<struct>_", [1000], 1000)),
("_update_name", typ "idt", NoSyn),
- ("_constrainAbs", typ "'a", NoSyn),
+ ("_constrainAbs", typ "'a", NoSyn),
("_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 _"),
(const "==>", typ "prop => prop => prop", Delimfix "op ==>"),
(const Term.dummy_patternN, typ "aprop", Delimfix "'_"),
("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),