
diff -r cc6e281d8f72 -r 0a36825b16c1 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Fri Aug 27 02:08:36 2010 +0800
+++ b/Nominal/NewParser.thy	Fri Aug 27 03:37:17 2010 +0800
@@ -434,7 +434,7 @@
 
   val alpha_bn_rsp = 
     if get_STEPS lthy > 20
-    then raw_alpha_bn_rsp alpha_bn_equivp_thms alpha_bn_imp_thms
+    then raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp_thms alpha_bn_imp_thms
     else raise TEST lthy6 
 
   (* noting the quot_respects lemmas *)




