--- a/Nominal/NewParser.thy	Mon Jun 21 15:41:59 2010 +0100
+++ b/Nominal/NewParser.thy	Tue Jun 22 13:05:00 2010 +0100
@@ -436,14 +436,24 @@
            alpha_intros alpha_induct alpha_cases 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
+    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 _ = 
-    if get_STEPS lthy > 12
+    if get_STEPS lthy > 13
     then true else raise TEST lthy4
 
   val bn_nos = map (fn (_, i, _) => i) raw_bn_info;