--- a/Nominal/NewAlpha.thy	Thu May 06 14:10:56 2010 +0200
+++ b/Nominal/NewAlpha.thy	Thu May 06 14:13:45 2010 +0200
@@ -35,6 +35,15 @@
 end;
 *}
 
+ML {*
+fun mk_binop2 ctxt s (l, r) =
+  Syntax.check_term ctxt (Const (s, dummyT) $ l $ r)
+*}
+
+ML {*
+fun mk_compound_fv' ctxt = foldr1 (mk_binop2 ctxt @{const_name prod_fv})
+fun mk_compound_alpha' ctxt = foldr1 (mk_binop2 ctxt @{const_name prod_rel})
+*}
 
 ML {*
 fun alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees
@@ -78,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