--- a/Nominal/nominal_dt_alpha.ML	Thu Aug 26 02:08:00 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Fri Aug 27 02:03:52 2010 +0800
@@ -110,7 +110,7 @@
      if member (op=) bodies i then [] 
      else [lookup alpha_bn_map bn $ nth args i $ nth args' i]
 
-(* generat the premises for an alpha rule; mk_frees is used
+(* generate the premises for an alpha rule; mk_frees is used
    if no binders are present *)
 fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause =
 let
@@ -626,6 +626,7 @@
   
   val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} 
     @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) 
+
 in
   alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct 
     (K (asm_full_simp_tac ss)) ctxt