--- a/Nominal/NewAlpha.thy	Thu May 06 13:25:37 2010 +0200
+++ b/Nominal/NewAlpha.thy	Thu May 06 14:13:05 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