--- a/Nominal/Ex/Lambda.thy	Mon Jun 18 14:50:02 2012 +0100
+++ b/Nominal/Ex/Lambda.thy	Thu Jul 12 10:11:32 2012 +0100
@@ -864,7 +864,7 @@
 
 lemma abs_same_binder:
   fixes t ta s sa :: "_ :: fs"
-  assumes "sort_of (atom x) = sort_of (atom y)"
+  and x y::"'a::at"
   shows "[[atom x]]lst. t = [[atom y]]lst. ta \<and> [[atom x]]lst. s = [[atom y]]lst. sa
      \<longleftrightarrow> [[atom x]]lst. (t, s) = [[atom y]]lst. (ta, sa)"
   by (cases "atom x = atom y") (auto simp add: Abs1_eq_iff assms fresh_Pair)
@@ -907,6 +907,7 @@
 
 consts P :: "lam \<Rightarrow> bool"
 
+(*
 nominal_primrec  
   A :: "lam => lam"
 where  
@@ -943,7 +944,7 @@
 apply(rule allI)
 apply(rule refl)
 oops
-
+*)
 end