# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273148025 -7200
# Node ID c1edd05f207fd467460d734e3104b2539587bc4e
# Parent  1c866b53eb3c4167d6ebb25c2b9b46bb1d049d72# Parent  db218886e67455ba5519c62ad1726410d8b7e38d
merge

diff -r db218886e674 -r c1edd05f207f Nominal/NewAlpha.thy
--- 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