diff -r e9b0728061a8 -r 24de7e548094 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Tue Jun 22 13:31:42 2010 +0100
+++ b/Nominal/NewParser.thy	Tue Jun 22 18:07:53 2010 +0100
@@ -436,44 +436,36 @@
            alpha_intros alpha_induct alpha_cases lthy_tmp'' 
     else raise TEST lthy4
 
+  val alpha_equivp_thms = 
+    if get_STEPS lthy > 12
+    then raw_prove_equivp alpha_trms alpha_refl_thms alpha_sym_thms alpha_trans_thms lthy_tmp''
+    else raise TEST lthy4
+
   (* proving alpha implies alpha_bn *)
   val _ = warning "Proving alpha implies bn"
 
   val alpha_bn_imp_thms = 
-    if get_STEPS lthy > 12
+    if get_STEPS lthy > 13
     then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy_tmp'' 
     else raise TEST lthy4
-
-
+  
   val _ = tracing ("alphas " ^ commas (map (Syntax.string_of_term lthy4) alpha_trms))
   val _ = tracing ("alpha_bns " ^ commas (map (Syntax.string_of_term lthy4) alpha_bn_trms))
   val _ = tracing ("alpha_refl\n" ^ 
     cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_refl_thms))
   val _ = tracing ("alpha_bn_imp\n" ^ 
     cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_bn_imp_thms))
+  val _ = tracing ("alpha_equivp\n" ^ 
+    cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_equivp_thms))
 
   (* old stuff *)
   val _ = 
-    if get_STEPS lthy > 13
-    then true else raise TEST lthy4
-
-  val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
-  val bns = raw_bn_funs ~~ bn_nos;
-
-  val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos
-
-  val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy4;
- 
-  val _ = tracing ("reflps\n" ^ 
-    cat_lines (map (Syntax.string_of_term lthy4 o prop_of) reflps))
-  
-  val _ = 
-    if get_STEPS lthy > 13
+    if get_STEPS lthy > 14
     then true else raise TEST lthy4
 
   val alpha_equivp =
     if !cheat_equivp then map (equivp_hack lthy4) alpha_trms
-    else build_equivps alpha_trms reflps alpha_induct
+    else build_equivps alpha_trms alpha_refl_thms alpha_induct
       inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy4;
 
   val qty_binds = map (fn (_, b, _, _) => b) dts;
@@ -488,6 +480,10 @@
           Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr);
   val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7;
   val _ = warning "Proving respects";
+
+  val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
+  val bns = raw_bn_funs ~~ bn_nos;
+
   val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_eqs (map fst bns) lthy8;
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
@@ -496,6 +492,9 @@
 
   fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
     else fvbv_rsp_tac alpha_induct raw_fv_defs lthy8 1;
+
+  val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos
+
   val fv_rsps = prove_fv_rsp fv_alpha_all alpha_trms fv_rsp_tac lthy9;
   val (fv_rsp_pre, lthy10) = fold_map
     (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv]
@@ -510,7 +509,7 @@
     alpha_bn_rsp_tac) alpha_bn_trms lthy11
   fun const_rsp_tac _ =
     let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a
-      in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
+      in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end
   val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
     const_rsp_tac) raw_consts lthy11a
     val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns)