--- a/Nominal/NewAlpha.thy	Sun May 02 16:00:52 2010 +0100
+++ b/Nominal/NewAlpha.thy	Sun May 02 16:01:45 2010 +0100
@@ -35,16 +35,6 @@
 end;
 *}
 
-ML {*
-fun mk_pair (fst, snd) =
-let
-  val ty1 = fastype_of fst
-  val ty2 = fastype_of snd
-  val c = HOLogic.pair_const ty1 ty2
-in
-  c $ fst $ snd
-end;
-*}
 
 ML {*
 fun alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees
@@ -65,8 +55,8 @@
   val rhs_binds = binds_fn args2 binds;
   val lhs_bodys = foldr1 HOLogic.mk_prod (map (nth args) bodys);
   val rhs_bodys = foldr1 HOLogic.mk_prod (map (nth args2) bodys);
-  val lhs = mk_pair (lhs_binds, lhs_bodys);
-  val rhs = mk_pair (rhs_binds, rhs_bodys);
+  val lhs = HOLogic.mk_prod (lhs_binds, lhs_bodys);
+  val rhs = HOLogic.mk_prod (rhs_binds, rhs_bodys);
   val body_dts = map (nth dts) bodys;
   fun fv_for_dt dt =
     if Datatype_Aux.is_rec_type dt