
diff -r ad03df7e8056 -r 25d2cdf7d7e4 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Mon Jun 07 11:46:26 2010 +0200
+++ b/Nominal/NewParser.thy	Wed Jun 09 15:14:16 2010 +0200
@@ -427,6 +427,8 @@
 
   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_trans\n" ^ 
+    cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_trans_thms))
 
   val _ = 
     if get_STEPS lthy > 11




