Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/nominal_dt_alpha.ML
changeset 2464 f4eba60cbd69
parent 2440 0a36825b16c1
child 2469 4a6e78bd9de9 
--- 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
nominal2