--- a/Nominal/Nominal2.thy	Fri Nov 12 01:20:53 2010 +0000
+++ b/Nominal/Nominal2.thy	Sat Nov 13 10:25:03 2010 +0000
@@ -315,7 +315,7 @@
     else raise TEST lthy3
 
   (* defining the permute_bn functions *)
-  val (_, _, lthy3b) = 
+  val (raw_perm_bns, raw_perm_bn_simps, 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
@@ -447,11 +447,18 @@
     then raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp_thms alpha_bn_imp_thms
     else raise TEST lthy6 
 
+  val raw_perm_bn_rsp =
+    if get_STEPS lthy > 21
+    then raw_perm_bn_rsp (alpha_trms @ alpha_bn_trms) raw_perm_bns alpha_induct 
+      alpha_intros raw_perm_bn_simps lthy6
+    else raise TEST lthy6
+
   (* noting the quot_respects lemmas *)
   val (_, lthy6a) = 
-    if get_STEPS lthy > 21
+    if get_STEPS lthy > 22
     then Local_Theory.note ((Binding.empty, [rsp_attr]),
-      raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ alpha_bn_rsp) lthy6
+      raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ 
+      alpha_bn_rsp @ raw_perm_bn_rsp) lthy6
     else raise TEST lthy6
 
   (* defining the quotient type *)
@@ -459,7 +466,7 @@
   val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts
      
   val (qty_infos, lthy7) = 
-    if get_STEPS lthy > 22
+    if get_STEPS lthy > 23
     then define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a
     else raise TEST lthy6a
 
@@ -492,7 +499,7 @@
     map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms
 
   val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = 
-    if get_STEPS lthy > 23
+    if get_STEPS lthy > 24
     then 
       lthy7
       |> define_qconsts qtys qconstrs_descr 
@@ -504,12 +511,12 @@
 
   (* definition of the quotient permfunctions and pt-class *)
   val lthy9 = 
-    if get_STEPS lthy > 24
+    if get_STEPS lthy > 25
     then define_qperms qtys qty_full_names tvs qperm_descr raw_perm_laws lthy8 
     else raise TEST lthy8
   
   val lthy9a = 
-    if get_STEPS lthy > 25
+    if get_STEPS lthy > 26
     then define_qsizes qtys qty_full_names tvs qsize_descr lthy9
     else raise TEST lthy9
 
@@ -526,7 +533,7 @@
     prod.cases} 
 
   val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = 
-    if get_STEPS lthy > 26
+    if get_STEPS lthy > 27
     then 
       lthy9a    
       |> lift_thms qtys [] alpha_distincts  
@@ -538,7 +545,7 @@
     else raise TEST lthy9a
 
   val ((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), lthyB) = 
-    if get_STEPS lthy > 27
+    if get_STEPS lthy > 28
     then
       lthyA 
       |> lift_thms qtys [] raw_size_eqvt
@@ -552,26 +559,26 @@
   (* supports lemmas *) 
   val _ = warning "Proving Supports Lemmas and fs-Instances"
   val qsupports_thms =
-    if get_STEPS lthy > 28
+    if get_STEPS lthy > 29
     then prove_supports lthyB qperm_simps qtrms
     else raise TEST lthyB
 
   (* finite supp lemmas *)
   val qfsupp_thms =
-    if get_STEPS lthy > 29
+    if get_STEPS lthy > 30
     then prove_fsupp lthyB qtys qinduct qsupports_thms
     else raise TEST lthyB
 
   (* fs instances *)
   val lthyC =
-    if get_STEPS lthy > 30
+    if get_STEPS lthy > 31
     then fs_instance qtys qty_full_names tvs qfsupp_thms lthyB
     else raise TEST lthyB
 
   (* fv - supp equality *)
   val _ = warning "Proving Equality between fv and supp"
   val qfv_supp_thms = 
-    if get_STEPS lthy > 31
+    if get_STEPS lthy > 32
     then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs 
       qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
     else []