diff -r ac7dff1194e8 -r 3a5ebb2fcdbf Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Mon Sep 20 21:52:45 2010 +0800
+++ b/Nominal/Nominal2.thy	Wed Sep 22 14:19:48 2010 +0800
@@ -563,8 +563,8 @@
   val _ = warning "Proving Equality between fv and supp"
   val qfv_supp_thms = 
     if get_STEPS lthy > 31
-    then prove_fv_supp qtys qfvs qfv_bns qalpha_bns qbn_defs qfv_defs qeq_iffs 
-      qperm_simps qfv_qbn_eqvts qinducts (flat raw_bclauses) lthyC
+    then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qbn_defs qfv_defs qeq_iffs 
+      qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
     else []