--- a/Nominal/Nominal2_Eqvt.thy	Wed Mar 03 12:48:05 2010 +0100
+++ b/Nominal/Nominal2_Eqvt.thy	Wed Mar 03 14:22:58 2010 +0100
@@ -251,7 +251,7 @@
   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt
   Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt
 
-  atom_eqvt
+  atom_eqvt add_perm_eqvt
 
 thm eqvts
 thm eqvts_raw

--- a/Nominal/Parser.thy	Wed Mar 03 12:48:05 2010 +0100
+++ b/Nominal/Parser.thy	Wed Mar 03 14:22:58 2010 +0100
@@ -245,10 +245,10 @@
   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms
     ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5;
-(*  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms 
+  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms
     (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6;
   val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc;
-  val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
+(*  val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
     inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy6;
   val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
   val qty_names = map (fn (_, b, _, _) => b) dts;

--- a/Nominal/Rsp.thy	Wed Mar 03 12:48:05 2010 +0100
+++ b/Nominal/Rsp.thy	Wed Mar 03 14:22:58 2010 +0100
@@ -146,6 +146,34 @@
 by auto
 
 ML {*
+  fun indtac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
+  fun all_eqvts ctxt =
+    Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
+  val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
+*}
+
+ML {*
+fun mk_minimal_ss ctxt =
+  Simplifier.context ctxt empty_ss
+    setsubgoaler asm_simp_tac
+    setmksimps (mksimps [])
+*}
+
+ML {*
+fun alpha_eqvt_tac induct simps ctxt =
+  indtac induct THEN_ALL_NEW
+  simp_tac ((mk_minimal_ss ctxt) addsimps simps) THEN_ALL_NEW
+  REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conjs THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps 
+    @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alpha_gen}) THEN_ALL_NEW
+  (split_conjs THEN_ALL_NEW TRY o resolve_tac
+    @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})
+  THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (@{thms permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt))
+*}
+
+ML {*
 fun build_alpha_eqvts funs perms simps induct ctxt =
 let
   val pi = Free ("p", @{typ perm});
@@ -158,17 +186,7 @@
     HOLogic.mk_imp (alpha $ arg $ arg2,
       (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2)))
   val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2))))
-  fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
-  (
-   (asm_full_simp_tac (HOL_ss addsimps 
-      ((Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))
-    THEN_ALL_NEW (REPEAT o etac conjE THEN' etac @{thm exi[of _ _ "p"]} THEN'
-      REPEAT o etac conjE THEN'
-      (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW
-      (asm_full_simp_tac HOL_ss) THEN_ALL_NEW
-      (etac @{thm alpha_gen_compose_eqvt[of _ _ _ _ "p"]}) THEN_ALL_NEW
-    (asm_full_simp_tac (HOL_ss addsimps 
-      ((Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps))))) 1
+  fun tac _ = alpha_eqvt_tac induct simps ctxt 1
   val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac
 in
   map (fn x => mp OF [x]) (HOLogic.conj_elims thm)

--- a/Nominal/Test.thy	Wed Mar 03 12:48:05 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 03 14:22:58 2010 +0100
@@ -14,42 +14,6 @@
 thm alpha_weird_raw.intros[no_vars]
 thm fv_weird_raw.simps[no_vars]
 
-lemma "alpha_weird_raw a b \<Longrightarrow> alpha_weird_raw (p \<bullet> a) (p \<bullet> b)"
-apply (erule alpha_weird_raw.induct)
-defer
-apply (simp add: alpha_weird_raw.intros)
-apply (simp add: alpha_weird_raw.intros)
-apply (simp only: permute_weird_raw.simps)
-apply (rule alpha_weird_raw.intros)
-apply (erule exi[of _ _ "p"])
-apply (erule exi[of _ _ "p"])
-apply (erule exi[of _ _ "p"])
-apply (erule exi[of _ _ "p"])
-apply (erule conjE)+
-apply (rule conjI)
-apply (erule alpha_gen_compose_eqvt[of _ _ _ _ "p"])
-apply (simp add: eqvts)
-apply (simp add: eqvts)
-apply (rule conjI)
-defer
-apply (erule alpha_gen_compose_eqvt[of _ _ _ _ "p"])
-apply (simp add: eqvts)
-apply (simp add: eqvts)
-apply (rule conjI)
-defer
-apply (simp add: supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt)
-apply(simp add: alpha_gen.simps)
-apply(erule conjE)+
-  apply(rule conjI)
-  apply(rule_tac ?p1="- p" in permute_eq_iff[THEN iffD1])
-apply (simp add: eqvts)
-  apply(rule conjI)
-  apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1])
-apply (simp add: eqvts add_perm_eqvt)
-apply (simp add: permute_eqvt[symmetric])
-done
-
-
 (*
 abbreviation "WBind \<equiv> WBind_raw"
 abbreviation "WP \<equiv> WP_raw"