--- a/Nominal/NewParser.thy	Sat Aug 14 23:33:23 2010 +0800
+++ b/Nominal/NewParser.thy	Sun Aug 15 11:03:13 2010 +0800
@@ -318,20 +318,18 @@
   val all_raw_ty_names = map (fst o dest_Type) all_raw_tys
   
   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_raw_ty_names  
-  val inject_thms = flat (map #inject dtinfos);
-  val distinct_thms = flat (map #distinct dtinfos);
-  val constr_thms = inject_thms @ distinct_thms
-  val rel_dtinfos = List.take (dtinfos, (length dts)); 
-  val raw_constrs_distinct = (map #distinct rel_dtinfos); 
+  val inject_thms = flat (map #inject dtinfos)
+  val distinct_thms = flat (map #distinct dtinfos)
+  val constr_thms = inject_thms @ distinct_thms 
+  
   val raw_induct_thm = #induct dtinfo;
   val raw_induct_thms = #inducts dtinfo;
   val exhaust_thms = map #exhaust dtinfos;
-  val raw_size_trms = map (fn ty => Const (@{const_name size}, ty --> @{typ nat})) all_raw_tys
+  val raw_size_trms = map size_const all_raw_tys
   val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names)
     |> `(fn thms => (length thms) div 2)
     |> uncurry drop
   
-
   (* definitions of raw permutations *)
   val _ = warning "Definition of raw permutations";
   val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) =
@@ -366,8 +364,8 @@
 
   (* definition of alpha-distinct lemmas *)
   val _ = warning "Distinct theorems";
-  val (alpha_distincts, alpha_bn_distincts) = 
-    mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info
+  val alpha_distincts = 
+    mk_alpha_distincts lthy4 alpha_cases distinct_thms alpha_trms all_raw_tys
 
   (* definition of alpha_eq_iff  lemmas *)
   (* they have a funny shape for the simplifier *)
@@ -563,7 +561,7 @@
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
   fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy
     else
-      let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts @ alpha_bn_distincts) alpha_equivp_thms exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
+      let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts) alpha_equivp_thms exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
   val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
     alpha_bn_rsp_tac) alpha_bn_trms lthy11
   fun const_rsp_tac _ =