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 2469 4a6e78bd9de9
parent 2464 f4eba60cbd69
child 2475 486d4647bb37 
--- a/Nominal/nominal_dt_alpha.ML	Sat Sep 04 06:23:31 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Sat Sep 04 06:48:14 2010 +0800
@@ -88,7 +88,7 @@
   val (alpha_name, binder_ty) = 
     case bmode of
       Lst => (@{const_name "alpha_lst"}, @{typ "atom list"})
-    | Set => (@{const_name "alpha_gen"}, @{typ "atom set"})
+    | Set => (@{const_name "alpha_set"}, @{typ "atom set"})
     | Res => (@{const_name "alpha_res"}, @{typ "atom set"})
   val ty = fastype_of args
   val pair_ty = HOLogic.mk_prodT (binder_ty, ty)
nominal2