diff -r 2bfd5be8578a -r 1c866b53eb3c Nominal/NewAlpha.thy
--- a/Nominal/NewAlpha.thy	Thu May 06 14:13:05 2010 +0200
+++ b/Nominal/NewAlpha.thy	Thu May 06 14:13:35 2010 +0200
@@ -87,7 +87,7 @@
   val t = Syntax.check_term lthy alpha_gen_ex
 in
   case binds of
-    [(SOME bn, i)] => if i mem bodys then [t]
+    [(SOME bn, i)] => if member (op =) bodys i then [t]
       else [t, ((the (AList.lookup (op=) bn_alphabn bn)) $ nth args i $ nth args2 i)]
     | _ => [t]
 end