--- a/Nominal/NewParser.thy	Tue Jun 22 13:05:00 2010 +0100
+++ b/Nominal/NewParser.thy	Tue Jun 22 13:31:42 2010 +0100
@@ -452,6 +452,7 @@
   val _ = tracing ("alpha_bn_imp\n" ^ 
     cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_bn_imp_thms))
 
+  (* old stuff *)
   val _ = 
     if get_STEPS lthy > 13
     then true else raise TEST lthy4
@@ -462,6 +463,14 @@
   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
+    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