--- a/Nominal/Fv.thy	Wed Mar 03 14:22:58 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 03 15:28:25 2010 +0100
@@ -1,5 +1,5 @@
 theory Fv
-imports "Nominal2_Atoms" "Abs" "Perm" (* For testing *)
+imports "Nominal2_Atoms" "Abs" "Perm" "Rsp" (* For testing *)
 begin
 
 (* Bindings are given as a list which has a length being equal
@@ -312,15 +312,16 @@
 *}
 
 ML {*
-fun reflp_tac induct inj =
+fun reflp_tac induct inj ctxt =
   rtac induct THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW
-(*  TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW*)
-  (rtac @{thm exI[of _ "0 :: perm"]} THEN'
-   asm_full_simp_tac (HOL_ss addsimps
-     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}))
+  simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW
+  split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
+  THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
+     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv
+       add_0_left supp_zero_perm Int_empty_left})
 *}
 
+
 lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi"
 apply (erule exE)
 apply (rule_tac x="-pi" in exI)
@@ -400,7 +401,7 @@
 let
   val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt;
   val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z)
-  fun reflp_tac' _ = reflp_tac term_induct alpha_inj 1;
+  fun reflp_tac' _ = reflp_tac term_induct alpha_inj ctxt 1;
   fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt 1;
   fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1;
   val reflt = Goal.prove ctxt' [] [] reflg reflp_tac';