--- a/Nominal/Abs.thy	Sat Mar 27 06:44:14 2010 +0100
+++ b/Nominal/Abs.thy	Sat Mar 27 06:44:47 2010 +0100
@@ -54,22 +54,25 @@
 fun
   alpha_abs 
 where
+  [simp del]:
   "alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
 
 fun
   alpha_abs_lst
 where
+  [simp del]:
   "alpha_abs_lst (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))"
 
 fun
   alpha_abs_res
 where
+  [simp del]:
   "alpha_abs_res (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op=) supp p (cs, y))"
 
 notation
-  alpha_abs ("_ \<approx>abs _") and
-  alpha_abs_lst ("_ \<approx>abs'_lst _") and
-  alpha_abs_res ("_ \<approx>abs'_res _")
+  alpha_abs (infix "\<approx>abs" 50) and
+  alpha_abs_lst (infix "\<approx>abs'_lst" 50) and
+  alpha_abs_res (infix "\<approx>abs'_res" 50)
 
 lemmas alphas_abs = alpha_abs.simps alpha_abs_res.simps alpha_abs_lst.simps
 
@@ -208,7 +211,7 @@
   shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
   and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)"
   and   "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)"
-  apply(simp_all)
+  apply(simp_all add: alphas_abs)
   apply(lifting alphas_abs)
   done