--- a/src/Pure/Syntax/mixfix.ML Wed Nov 07 18:18:29 2001 +0100
+++ b/src/Pure/Syntax/mixfix.ML Wed Nov 07 18:18:46 2001 +0100
@@ -202,7 +202,7 @@
val pure_nonterms =
(Lexicon.terminals @ [SynExt.logic, "type", "types", "sort", "classes",
SynExt.args, SynExt.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
- "asms", SynExt.any, SynExt.sprop]);
+ "asms", SynExt.any, SynExt.sprop, "struct", "structs"]);
val pure_syntax =
[("_lambda", "[pttrns, 'a] => logic", Mixfix ("(3%_./ _)", [0, 3], 3)),
@@ -232,7 +232,11 @@
("", "id => logic", Delimfix "_"),
("", "longid => logic", Delimfix "_"),
("", "var => logic", Delimfix "_"),
- ("_DDDOT", "logic", Delimfix "...")];
+ ("_DDDOT", "logic", Delimfix "..."),
+ ("_struct_app", "structs => logic => logic", Mixfix ("__", [0, 1000], 999)),
+ ("", "struct => structs", Delimfix "_"),
+ ("_structs", "struct => structs => structs", Delimfix "__"),
+ ("_struct", "struct", Delimfix "\\<struct>")];
val pure_appl_syntax =
[("_appl", "[('b => 'a), args] => logic", Mixfix ("(1_/(1'(_')))", [SynExt.max_pri, 0], SynExt.max_pri)),