--- a/Nominal/NewParser.thy	Mon May 24 21:11:33 2010 +0100
+++ b/Nominal/NewParser.thy	Tue May 25 00:24:41 2010 +0100
@@ -305,6 +305,8 @@
 
 setup STEPS_setup
 
+ML {* dtyp_no_of_typ *}
+
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 let
@@ -327,6 +329,9 @@
   val induct_thm = #induct dtinfo;
   val exhaust_thms = map #exhaust dtinfos;
 
+  val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
+  val bns = raw_bn_funs ~~ bn_nos;
+
   (* definitions of raw permutations *)
   val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) =
     if get_STEPS lthy1 > 2 
@@ -354,16 +359,12 @@
     then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3a
     else raise TEST lthy3a
   
-  val dts_names = map (fn (i, (s, _, _)) => (s, i)) descr;
-  val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
-  val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
- 
-  val bns = raw_bn_funs ~~ bn_nos;
+  (* HERE *)
+  (* definition of raw_alpha_eq_iff  lemmas *)
   val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) (rel_distinct ~~ alpha_ts));
   val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
     ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_bn_ts))
-  
-  (* definition of raw_alpha_eq_iff  lemmas *)
+ 
   val alpha_eq_iff = 
     if get_STEPS lthy > 5
     then build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4
@@ -375,7 +376,7 @@
   val _ = warning "Proving equivariance";
   val (bv_eqvt, lthy5) = 
     if get_STEPS lthy > 6
-    then prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) (map fst bns) lthy4
+    then prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) raw_bn_funs lthy4
     else raise TEST lthy4
 
   val (fv_eqvt, lthy6) =