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 2299 09bbed4f21d6
parent 2298 aead2aad845c
child 2300 9fb315392493 
--- a/Nominal/nominal_dt_alpha.ML	Mon May 24 21:11:33 2010 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Tue May 25 00:24:41 2010 +0100
@@ -210,8 +210,8 @@
   val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) constrs_info bclausesss 
   val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss) bn_info
 
-  val all_alpha_names = map2 (fn s => fn ty => ((Binding.name s, ty), NoSyn))
-    (alpha_names @ alpha_bn_names) (alpha_tys @ alpha_bn_tys)
+  val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn))
+    (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)
   val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
   
   val (alphas, lthy') = Inductive.add_inductive_i
nominal2