diff -r 217149972715 -r f4eba60cbd69 Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Fri Sep 03 20:53:09 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Fri Sep 03 22:22:43 2010 +0800
@@ -64,7 +64,7 @@
 end
 
 (* generates the compound binder terms *)
-fun mk_binders lthy bmode args bodies = 
+fun mk_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)
@@ -77,7 +77,7 @@
     | Set => (mk_union,  bind_set)
     | Res => (mk_union,  bind_set)
 in
-  bodies
+  binders
   |> map (bind_fn lthy args)
   |> foldl1 combine_fn 
 end