# HG changeset patch
# User wenzelm
# Date 1005153526 -3600
# Node ID 935e29914f93d0c74d245d717b666d700fe1e236
# Parent  db9a3ad6e90e05890d4f51c197419354ba90bed7
syntax for structs;

diff -r db9a3ad6e90e -r 935e29914f93 src/Pure/Syntax/mixfix.ML
--- 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)),