--- a/Nominal/Nominal2.thy	Mon Nov 15 08:17:11 2010 +0000
+++ b/Nominal/Nominal2.thy	Mon Nov 15 09:52:29 2010 +0000
@@ -586,6 +586,12 @@
       qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
     else []
 
+  (* proving that the qbn result is finite *)
+  val qbn_finite_thms =
+    if get_STEPS lthy > 33
+    then prove_bns_finite qtys qbns qinduct qbn_defs lthyC
+    else []
+
   (* postprocessing of eq and fv theorems *)
 
   val qeq_iffs' = qeq_iffs
@@ -632,6 +638,7 @@
      ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs)
      ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros)
      ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps)
+     ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms)
 in
   (0, lthy9')
 end handle TEST ctxt => (0, ctxt)