diff -r 559419060d99 -r 278253330b6a Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Tue Feb 02 12:36:01 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Tue Feb 02 12:48:12 2010 +0100
@@ -53,7 +53,7 @@
   "(alpha_gen (bs, x) R f pi (cs, y)) \<longleftrightarrow> (f x - bs = f y - cs) \<and> ((f x - bs) \<sharp>* pi) \<and> (R (pi \<bullet> x) y)"
 
 notation
-  alpha_gen ("_ \<approx>gen _ _ _ _")
+  alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100)
 
 lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2"
   by (cases x) (auto simp add: le_fun_def le_bool_def alpha_gen.simps)
@@ -71,7 +71,7 @@
 
 lemma alpha_gen_atom_sym:
   assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "\<exists>pi. ({atom a}, t) \<approx>gen \<lambda>x1 x2. R x1 x2 \<and> R x2 x1 f pi ({atom b}, s) \<Longrightarrow>
+  shows "\<exists>pi. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi ({atom b}, s) \<Longrightarrow>
         \<exists>pi. ({atom b}, s) \<approx>gen R f pi ({atom a}, t)"
   apply(erule exE)
   apply(rule_tac x="- pi" in exI)
@@ -97,7 +97,7 @@
 
 lemma alpha_gen_atom_trans:
   assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "\<lbrakk>\<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen \<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x) f pi ({atom aa}, ta);
+  shows "\<lbrakk>\<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi ({atom aa}, ta);
         \<exists>pi\<Colon>perm. ({atom aa}, ta) \<approx>gen R f pi ({atom ba}, sa)\<rbrakk>
     \<Longrightarrow> \<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen R f pi ({atom ba}, sa)"
   apply(simp add: alpha_gen.simps)
@@ -131,7 +131,7 @@
 
 lemma alpha_gen_atom_eqvt:
   assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
-  and     b: "\<exists>pia. ({atom a}, t) \<approx>gen \<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2) f pia ({atom b}, s)"
+  and     b: "\<exists>pia. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia ({atom b}, s)"
   shows  "\<exists>pia. ({atom (pi \<bullet> a)}, pi \<bullet> t) \<approx>gen R f pia ({atom (pi \<bullet> b)}, pi \<bullet> s)"
   using b apply -
   apply(erule exE)