# HG changeset patch
# User wenzelm
# Date 874942182 -7200
# Node ID 3f7053bf423756bd88b88050397499d4acaed1cc
# Parent  73378599a65b27f70ab52aa7e845b5a6f0d3e70d
fixed idt/idts vs. pttrn/pttrns;

diff -r 73378599a65b -r 3f7053bf4237 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Mon Sep 22 16:08:45 1997 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Mon Sep 22 17:29:42 1997 +0200
@@ -156,19 +156,21 @@
 val pure_types =
   map (fn t => (t, 0, NoSyn))
     (terminals @ [logic, "type", "types", "sort", "classes", args, cargs,
-      "pttrn", "idt", "idts", "aprop", "asms", any, sprop, "dummy"]);
+      "pttrn", "pttrns", "idt", "idts", "aprop", "asms", any, sprop, "dummy"]);
 
 val pure_syntax =
- [("_lambda",      "[idts, 'a] => logic",           Mixfix ("(3%_./ _)", [0, 3], 3)),
+ [("_lambda",      "[pttrns, 'a] => logic",         Mixfix ("(3%_./ _)", [0, 3], 3)),
   ("_abs",         "'a",                            NoSyn),
   ("",             "'a => " ^ args,                 Delimfix "_"),
   ("_args",        "['a, " ^ args ^ "] => " ^ args, Delimfix "_,/ _"),
   ("",             "id => idt",                     Delimfix "_"),
   ("_idtyp",       "[id, type] => idt",             Mixfix ("_::_", [], 0)),
   ("",             "idt => idt",                    Delimfix "'(_')"),
+  ("",             "idt => idts",                   Delimfix "_"),
+  ("_idts",        "[idt, idts] => idts",           Mixfix ("_/ _", [1, 0], 0)),
   ("",             "idt => pttrn",                  Delimfix "_"),
-  ("",             "pttrn => idts",                 Delimfix "_"),
-  ("_idts",        "[pttrn, idts] => idts",         Mixfix ("_/ _", [1, 0], 0)),
+  ("",             "pttrn => pttrns",               Delimfix "_"),
+  ("_pttrns",      "[pttrn, pttrns] => pttrns",     Mixfix ("_/ _", [1, 0], 0)),
   ("",             "id => aprop",                   Delimfix "_"),
   ("",             "var => aprop",                  Delimfix "_"),
   ("_aprop",       "aprop => prop",                 Delimfix "PROP _"),
@@ -198,7 +200,7 @@
   ("_ofsort",  "[tid, sort] => type",   Mixfix ("_\\<Colon>_", [max_pri, 0], max_pri)),
   ("_constrain", "['a, type] => 'a",    Mixfix ("_\\<Colon>_", [4, 0], 3)),
   ("_idtyp",   "[id, type] => idt",     Mixfix ("_\\<Colon>_", [], 0)),
-  ("_lambda",  "[idts, 'a] => logic",   Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
+  ("_lambda",  "[pttrns, 'a] => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
   ("==>",      "[prop, prop] => prop",  InfixrName ("\\<Midarrow>\\<Rightarrow>", 1)),
   ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((3\\<lbrakk>_\\<rbrakk>)/ \\<Midarrow>\\<Rightarrow> _)", [0, 1], 1)),
   ("==",       "['a::{}, 'a] => prop",  InfixrName ("\\<equiv>", 2)),