diff -r 7b1470b55936 -r 4a6e78bd9de9 Nominal/nominal_dt_alpha.ML
--- 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)