diff -r 0f289a52edbe -r b136721eedb2 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Tue Dec 07 14:27:21 2010 +0000
+++ b/Nominal/Nominal2.thy	Tue Dec 07 14:27:39 2010 +0000
@@ -1,15 +1,11 @@
 theory Nominal2
 imports 
   Nominal2_Base Nominal2_Eqvt Nominal2_Abs
-uses ("nominal_dt_rawperm.ML")
-     ("nominal_dt_rawfuns.ML")
+uses ("nominal_dt_rawfuns.ML")
      ("nominal_dt_alpha.ML")
      ("nominal_dt_quot.ML")
 begin
 
-use "nominal_dt_rawperm.ML"
-ML {* open Nominal_Dt_RawPerm *}
-
 use "nominal_dt_rawfuns.ML"
 ML {* open Nominal_Dt_RawFuns *}
 
@@ -614,6 +610,12 @@
       qalpha_refl_thms lthyC
     else []
 
+  (* proving the relationship of bn and permute_bn *)
+  val qpermute_bn_thms = 
+    if get_STEPS lthy > 33
+    then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC
+    else []
+
   (* noting the theorems *)  
 
   (* generating the prefix for the theorem names *)
@@ -641,6 +643,7 @@
      ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps)
      ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms)
      ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms)
+     ||>> Local_Theory.note ((thms_suffix "permute_bn", []), qpermute_bn_thms)
 in
   (0, lthy9')
 end handle TEST ctxt => (0, ctxt)