--- a/Nominal/Nominal2.thy	Wed Sep 22 18:13:26 2010 +0200
+++ b/Nominal/Nominal2.thy	Wed Sep 22 23:17:25 2010 +0200
@@ -563,7 +563,7 @@
   val _ = warning "Proving Equality between fv and supp"
   val qfv_supp_thms = 
     if get_STEPS lthy > 31
-    then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qbn_defs qfv_defs qeq_iffs 
+    then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs 
       qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
     else []
 

--- a/Nominal/nominal_dt_supp.ML	Wed Sep 22 18:13:26 2010 +0200
+++ b/Nominal/nominal_dt_supp.ML	Wed Sep 22 23:17:25 2010 +0200
@@ -13,7 +13,7 @@
   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 -> 
+  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 
 end
 
@@ -155,14 +155,12 @@
 fun q_tac msg i = 
   if true then print_tac ("qtest: " ^ msg) else all_tac
 
-fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns bn_simps fv_simps eq_iffs perm_simps 
+fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps 
   fv_bn_eqvts qinduct bclausess ctxt =
   let
     val goals1 = map mk_fvs_goals fvs
     val goals2 = map2 mk_fv_bns_goals fv_bns alpha_bns   
 
-    
-
     fun tac ctxt =
       SUBGOAL (fn (goal, i) =>
         let
@@ -190,55 +188,6 @@
     induct_prove qtys (goals1 @ goals2) qinduct tac ctxt
   end
 
-(*
-   fun fv_tac bclauses ctxt =
-      SOLVED' (EVERY' [
-        (fn i => print_tac ("FV Goal: " ^ string_of_int i ^ "  with  " ^ (@{make_string} bclauses))),
-        TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), 
-        p_tac "A",
-        TRY o EVERY' (mk_supp_abs_tac ctxt bclauses),
-        p_tac "B",
-        TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}),
-        p_tac "C",
-        TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], 
-        p_tac "D",
-        TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)),
-        p_tac "E",
-        TRY o asm_full_simp_tac (add_ss thms3),
-        p_tac "F",
-        TRY o simp_tac (add_ss thms2),
-        p_tac "G",
-        TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts))),
-        p_tac "H",
-        (fn i => print_tac ("finished with FV Goal: " ^ string_of_int i))
-        ])
-    
-    fun fv_tacs ctxt = map (fv_tac ctxt) bclausess
-    (*fun bn_tacs ctxt = map (bn_tac ctxt) bn_simps*)
-*)
-
-(*
-  fun bn_tac ctxt bn_simp =
-      SOLVED' (EVERY' [
-        (fn i => print_tac ("BN Goal: " ^ string_of_int i)),
-        TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)),
-        q_tac "A",
-        TRY o mk_bn_supp_abs_tac bn_simp,
-        q_tac "B",
-        TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}),
-        q_tac "C",
-        TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], 
-        q_tac "D",
-        TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)),
-        q_tac "E",
-        TRY o asm_full_simp_tac (add_ss thms3),
-        q_tac "F",
-        TRY o simp_tac (add_ss thms2),
-        q_tac "G",
-        TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts))),
-        (fn i => print_tac ("finished with BN Goal: " ^ string_of_int i))
-        ])
-*)
 
 
 end (* structure *)