--- a/Nominal/nominal_dt_supp.ML	Mon Dec 06 16:35:42 2010 +0000
+++ b/Nominal/nominal_dt_supp.ML	Mon Dec 06 17:11:34 2010 +0000
@@ -7,18 +7,7 @@
 
 signature NOMINAL_DT_SUPP =
 sig
-  val prove_supports: Proof.context -> thm list -> term list -> thm list  
-  val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list
-
-  val fs_instance: typ list -> string list -> (string * sort) list -> thm list ->  
-    local_theory -> local_theory
-
-  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
-  val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list ->
-    thm list -> Proof.context -> thm list
+  
 end
 
 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
@@ -217,8 +206,8 @@
       end
 
     val props = map2 mk_goal qperm_bns alpha_bns
-    val ss_tac = (K (print_tac "test")) THEN' 
-      asm_full_simp_tac (HOL_ss addsimps (@{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls))
+    val ss = @{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls
+    val ss_tac = asm_full_simp_tac (HOL_ss addsimps ss)
   in
     induct_prove qtys props qinduct (K ss_tac) ctxt'
     |> ProofContext.export ctxt' ctxt