diff -r 6b51117b8955 -r 217ef3e4282e Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Sun Aug 29 00:36:47 2010 +0800
+++ b/Nominal/NewParser.thy	Sun Aug 29 01:17:36 2010 +0800
@@ -547,6 +547,11 @@
     then prove_supports lthyB qperm_simps qtrms
     else raise TEST lthyB
 
+  val qfsupp_thms =
+    if get_STEPS lthy > 29
+    then prove_fsupp lthyB qtys qinduct qsupports_thms
+    else raise TEST lthyB
+
 
   (* noting the theorems *)  
 
@@ -566,7 +571,7 @@
      ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) 
      ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
      ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
-     
+     ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
 in
   (0, lthy9')
 end handle TEST ctxt => (0, ctxt)