diff -r 3885dc2669f9 -r abafea9b39bb Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Thu Aug 26 02:08:00 2010 +0800
+++ b/Nominal/NewParser.thy	Fri Aug 27 02:03:52 2010 +0800
@@ -330,7 +330,7 @@
     mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_tys
 
   (* definition of alpha_eq_iff  lemmas *)
-  (* they have a funny shape for the simplifier *)
+  (* they have a funny shape for the simplifier ---- CHECK WHETHER NEEDED*)
   val _ = warning "Eq-iff theorems";
   val (alpha_eq_iff_simps, alpha_eq_iff) = 
     if get_STEPS lthy > 5
@@ -402,24 +402,44 @@
     else raise TEST lthy6
   
   (* respectfulness proofs *)
-  val raw_funs_rsp_aux = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs 
-    raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy6
-  val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux
+  val raw_funs_rsp_aux = 
+    if get_STEPS lthy > 15
+    then raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs 
+      raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy6
+    else raise TEST lthy6 
+  
+  val raw_funs_rsp = 
+    if get_STEPS lthy > 16
+    then map mk_funs_rsp raw_funs_rsp_aux
+    else raise TEST lthy6 
 
-  val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct 
-    (raw_size_thms @ raw_size_eqvt) lthy6
-    |> map mk_funs_rsp
+  val raw_size_rsp = 
+    if get_STEPS lthy > 17
+    then
+      raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct 
+      (raw_size_thms @ raw_size_eqvt) lthy6
+      |> map mk_funs_rsp
+    else raise TEST lthy6 
 
-  val raw_constrs_rsp = raw_constrs_rsp raw_constrs alpha_trms alpha_intros
-    (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 
+  val raw_constrs_rsp = 
+    if get_STEPS lthy > 18
+    then raw_constrs_rsp raw_constrs alpha_trms alpha_intros
+      (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 
+    else raise TEST lthy6 
 
-  val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt
+  val alpha_permute_rsp = 
+    if get_STEPS lthy > 19
+    then map mk_alpha_permute_rsp alpha_eqvt
+    else raise TEST lthy6 
 
-  val alpha_bn_rsp = raw_alpha_bn_rsp alpha_bn_equivp_thms alpha_bn_imp_thms
+  val alpha_bn_rsp = 
+    if get_STEPS lthy > 20
+    then raw_alpha_bn_rsp alpha_bn_equivp_thms alpha_bn_imp_thms
+    else raise TEST lthy6 
 
   (* noting the quot_respects lemmas *)
   val (_, lthy6a) = 
-    if get_STEPS lthy > 15
+    if get_STEPS lthy > 21
     then Local_Theory.note ((Binding.empty, [rsp_attrib]),
       raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ alpha_bn_rsp) lthy6
     else raise TEST lthy6
@@ -429,7 +449,7 @@
   val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts
      
   val (qty_infos, lthy7) = 
-    if get_STEPS lthy > 16
+    if get_STEPS lthy > 22
     then define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a
     else raise TEST lthy6a
 
@@ -462,7 +482,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 > 17
+    if get_STEPS lthy > 23
     then 
       lthy7
       |> define_qconsts qtys qconstrs_descr 
@@ -474,12 +494,12 @@
 
   (* definition of the quotient permfunctions and pt-class *)
   val lthy9 = 
-    if get_STEPS lthy > 18
+    if get_STEPS lthy > 24
     then define_qperms qtys qty_full_names tvs qperm_descr raw_perm_laws lthy8 
     else raise TEST lthy8
   
   val lthy9a = 
-    if get_STEPS lthy > 19
+    if get_STEPS lthy > 25
     then define_qsizes qtys qty_full_names tvs qsize_descr lthy9
     else raise TEST lthy9
 
@@ -496,7 +516,7 @@
     prod.cases} 
 
   val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = 
-    if get_STEPS lthy > 20
+    if get_STEPS lthy > 26
     then 
       lthy9a    
       |> lift_thms qtys [] alpha_distincts  
@@ -508,7 +528,7 @@
     else raise TEST lthy9a
 
   val (((qsize_eqvt, [qinduct]), qexhausts), lthyB) = 
-    if get_STEPS lthy > 20
+    if get_STEPS lthy > 27
     then
       lthyA 
       |> lift_thms qtys [] raw_size_eqvt