diff -r add799cf0817 -r 82e37a4595c7 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Wed Nov 10 13:46:21 2010 +0000
+++ b/Nominal/Nominal2.thy	Fri Nov 12 01:20:53 2010 +0000
@@ -169,6 +169,7 @@
   in
     (dt_index, (bn_fun, (cnstr_head, rhs_elements)))
   end
+
   fun order dts i ts = 
   let
     val dt = nth dts i
@@ -190,7 +191,6 @@
   ordered'
 end
 
-
 fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy =
   if null raw_bn_funs 
   then ([], [], [], [], lthy)
@@ -210,6 +210,7 @@
     in
       (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2)
     end
+
 *}
 
 ML {*
@@ -298,33 +299,40 @@
   (* definitions of raw permutations by primitive recursion *)
   val _ = warning "Definition of raw permutations";
   val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) =
-    if get_STEPS lthy0 > 1 
+    if get_STEPS lthy0 > 0 
     then define_raw_perms raw_full_ty_names raw_tys tvs raw_constrs raw_induct_thm lthy0
     else raise TEST lthy0
  
   (* noting the raw permutations as eqvt theorems *)
   val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a
 
-  (* definition of raw fv_functions *)
-  val _ = warning "Definition of raw fv-functions";
+  (* definition of raw fv and bn functions *)
+  val _ = warning "Definition of raw fv- and bn-functions";
   val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) =
-    if get_STEPS lthy3 > 2 
+    if get_STEPS lthy3 > 1
     then define_raw_bns raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs 
       (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3
     else raise TEST lthy3
 
-  val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = 
-    if get_STEPS lthy3a > 3 
-    then define_raw_fvs raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses 
+  (* defining the permute_bn functions *)
+  val (_, _, lthy3b) = 
+    if get_STEPS lthy3a > 2
+    then define_raw_bn_perms raw_tys raw_bn_info raw_cns_info 
       (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3a
     else raise TEST lthy3a
 
+  val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3c) = 
+    if get_STEPS lthy3b > 3 
+    then define_raw_fvs raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses 
+      (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b
+    else raise TEST lthy3b
+
   (* definition of raw alphas *)
   val _ = warning "Definition of alphas";
   val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) =
-    if get_STEPS lthy3b > 4 
-    then define_raw_alpha raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3b
-    else raise TEST lthy3b
+    if get_STEPS lthy3c > 4 
+    then define_raw_alpha raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c
+    else raise TEST lthy3c
   val alpha_tys = map (domain_type o fastype_of) alpha_trms  
 
   (* definition of alpha-distinct lemmas *)