diff -r 1c77e15c4259 -r f0252365936c Nominal/nominal_dt_supp.ML
--- a/Nominal/nominal_dt_supp.ML	Mon Nov 15 08:17:11 2010 +0000
+++ b/Nominal/nominal_dt_supp.ML	Mon Nov 15 09:52:29 2010 +0000
@@ -15,6 +15,9 @@
 
   val prove_fv_supp: typ list -> term list -> term list -> term list -> term list -> thm list -> 
     thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list 
+
+  val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list
+
 end
 
 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
@@ -145,7 +148,7 @@
 val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc}
 val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un}
 val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def 
-  prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] Finite_Set.finite.emptyI}
+  prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI}
 
 fun p_tac msg i = 
   if false then print_tac ("ptest: " ^ msg) else all_tac
@@ -189,5 +192,22 @@
   end
 
 
+fun prove_bns_finite qtys qbns qinduct qbn_simps ctxt =
+  let
+    fun mk_goal qbn = 
+      let
+        val arg_ty = domain_type (fastype_of qbn)
+        val finite = @{term "finite :: atom set => bool"}
+      in
+        (arg_ty, fn x => finite $ (to_set (qbn $ x)))
+      end
+
+    val props = map mk_goal qbns
+    val ss_tac = asm_full_simp_tac (HOL_basic_ss addsimps (qbn_simps @ 
+      @{thms set.simps set_append finite_insert finite.emptyI finite_Un}))
+  in
+    induct_prove qtys props qinduct (K (ss_tac ORELSE' (K no_tac))) ctxt
+  end
+
 
 end (* structure *)