--- a/Nominal/Nominal2.thy	Wed Sep 22 18:13:26 2010 +0200
+++ b/Nominal/Nominal2.thy	Wed Sep 22 23:17:25 2010 +0200
@@ -563,7 +563,7 @@
   val _ = warning "Proving Equality between fv and supp"
   val qfv_supp_thms = 
     if get_STEPS lthy > 31
-    then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qbn_defs qfv_defs qeq_iffs 
+    then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs 
       qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
     else []