--- a/Nominal/Ex/Lambda.thy	Wed Apr 14 15:02:07 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Wed Apr 14 16:05:58 2010 +0200
@@ -174,10 +174,10 @@
   tt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"  
   for r :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
 where
-    "tt r a b"
-  | "tt r a b ==> tt r a c"
+    aa: "tt r a a"
+  | bb: "tt r a b ==> tt r a c"
 
-(*
+(* PROBLEM: derived eqvt-theorem does not conform with [eqvt]
 equivariance tt
 *)