# HG changeset patch
# User oheimb
# Date 861871140 -7200
# Node ID ce99919010bfc86863ed0300d490085a357b1b6f
# Parent  7a5611f66b7286349d671f1fafec55ef996e18b3
changed priority of '%': now no parenteses needed for '[...] == %x. [...]'

diff -r 7a5611f66b72 -r ce99919010bf src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Thu Apr 24 09:34:59 1997 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Thu Apr 24 10:39:00 1997 +0200
@@ -159,7 +159,7 @@
       "pttrn", "idt", "idts", "aprop", "asms", any, sprop, "dummy"]);
 
 val pure_syntax =
- [("_lambda",      "[idts, 'a] => logic",           Mixfix ("(3%_./ _)", [], 0)),
+ [("_lambda",      "[idts, 'a] => logic",           Mixfix ("(3%_./ _)", [0, 3], 3)),
   ("_abs",         "'a",                            NoSyn),
   ("",             "'a => " ^ args,                 Delimfix "_"),
   ("_args",        "['a, " ^ args ^ "] => " ^ args, Delimfix "_,/ _"),
@@ -198,7 +198,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)),
+  ("_lambda",  "[idts, '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)),