--- a/Nominal/nominal_dt_alpha.ML	Thu Dec 16 02:25:35 2010 +0000
+++ b/Nominal/nominal_dt_alpha.ML	Thu Dec 16 08:42:48 2010 +0000
@@ -7,6 +7,8 @@
 
 signature NOMINAL_DT_ALPHA =
 sig
+  val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term
+
   val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> 
     bclause list list list -> term list -> Proof.context -> 
     term list * term list * thm list * thm list * thm * local_theory
@@ -71,7 +73,7 @@
   end
 
 (* generates the compound binder terms *)
-fun mk_binders lthy bmode args binders = 
+fun comb_binders lthy bmode args binders = 
   let  
     fun bind_set lthy args (NONE, i) = setify lthy (nth args i)
       | bind_set _ args (SOME bn, i) = bn $ (nth args i)
@@ -150,8 +152,8 @@
           val comp_alpha = foldl1 mk_prod_alpha alphas
           val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies)
           val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies)
-          val comp_binders = mk_binders lthy bmode args binders
-          val comp_binders' = mk_binders lthy bmode args' binders
+          val comp_binders = comb_binders lthy bmode args binders
+          val comp_binders' = comb_binders lthy bmode args' binders
           val alpha_prem = 
             mk_alpha_term bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders'
           val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders)