--- a/Nominal/Atoms.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Atoms.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -210,7 +210,7 @@
   shows "ty_of (p \<bullet> x) = ty_of x"
   unfolding ty_of_def
   unfolding atom_eqvt [symmetric]
-  by simp
+  by (simp only: sort_of_permute)
 
 
 section {* Tests with subtyping and automatic coercions *}
@@ -236,6 +236,7 @@
 lemma
   fixes as::"var1 set"
   shows "atom ` as \<sharp>* t"
+
 oops
 
 end

--- a/Nominal/Ex/Classical.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Ex/Classical.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -83,21 +83,28 @@
   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
+  apply(simp add: atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(clarify)
+  apply(simp add: eqvt_at_def)
+  apply(simp add: atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(elim conjE)
   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
+  apply(simp add: atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
+  apply(simp add: atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(elim conjE)
   apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -105,7 +112,9 @@
   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(rule conjI)
   apply(elim conjE)
@@ -114,7 +123,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -124,7 +135,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -132,13 +145,17 @@
   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(elim conjE)
   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(elim conjE)
   apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
@@ -146,7 +163,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -156,7 +175,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -167,7 +188,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -177,7 +200,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -189,7 +214,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)  
@@ -197,8 +224,11 @@
   apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
+  apply(simp add: eqvt_at_def)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -210,7 +240,9 @@
   apply(simp add: Abs_fresh_star)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -254,19 +286,25 @@
   apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(elim conjE)
   apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(elim conjE)
   apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(elim conjE)
   apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)")
@@ -274,7 +312,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -285,7 +325,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -294,7 +336,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -304,7 +348,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -314,7 +360,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -322,13 +370,17 @@
   apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(elim conjE)
   apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(elim conjE)
   apply(rule conjI)
@@ -337,7 +389,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -346,7 +400,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -355,7 +411,9 @@
   apply(simp add: Abs_fresh_star)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(erule conjE)+
   apply(rule conjI)
@@ -364,7 +422,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -373,7 +433,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)

--- a/Nominal/Ex/Lambda.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Ex/Lambda.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -40,7 +40,6 @@
 | "is_app (App t1 t2) = True"
 | "is_app (Lam [x]. t) = False"
 apply(simp add: eqvt_def is_app_graph_def)
-apply (rule, perm_simp, rule)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)[3]
@@ -61,7 +60,6 @@
 | "rator (App t1 t2) = Some t1"
 | "rator (Lam [x]. t) = None"
 apply(simp add: eqvt_def rator_graph_def)
-apply (rule, perm_simp, rule)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)[3]
@@ -77,7 +75,6 @@
 | "rand (App t1 t2) = Some t2"
 | "rand (Lam [x]. t) = None"
 apply(simp add: eqvt_def rand_graph_def)
-apply (rule, perm_simp, rule)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)[3]
@@ -94,7 +91,6 @@
 | "is_eta_nf (Lam [x]. t) = (is_eta_nf t \<and> 
                              ((is_app t \<and> rand t = Some (Var x)) \<longrightarrow> atom x \<in> supp (rator t)))"
 apply(simp add: eqvt_def is_eta_nf_graph_def)
-apply (rule, perm_simp, rule)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)[3]
@@ -102,11 +98,7 @@
 apply(erule_tac c="()" in Abs_lst1_fcb2')
 apply(simp_all add: pure_fresh fresh_star_def)[3]
 apply(simp add: eqvt_at_def conj_eqvt)
-apply(perm_simp)
-apply(rule refl)
 apply(simp add: eqvt_at_def conj_eqvt)
-apply(perm_simp)
-apply(rule refl)
 done
 
 termination (eqvt) by lexicographic_order
@@ -128,7 +120,6 @@
 | "var_pos y (App t1 t2) = (Cons Left ` (var_pos y t1)) \<union> (Cons Right ` (var_pos y t2))"
 | "atom x \<sharp> y \<Longrightarrow> var_pos y (Lam [x]. t) = (Cons In ` (var_pos y t))"
 apply(simp add: eqvt_def var_pos_graph_def)
-apply (rule, perm_simp, rule)
 apply(rule TrueI)
 apply(case_tac x)
 apply(rule_tac y="b" and c="a" in lam.strong_exhaust)
@@ -138,12 +129,14 @@
 apply(erule_tac Abs_lst1_fcb2)
 apply(simp add: pure_fresh)
 apply(simp add: fresh_star_def)
-apply(simp add: eqvt_at_def image_eqvt perm_supp_eq)
+apply(simp only: eqvt_at_def)
 apply(perm_simp)
-apply(rule refl)
-apply(simp add: eqvt_at_def image_eqvt perm_supp_eq)
+apply(simp)
+apply(simp add: perm_supp_eq)
+apply(simp only: eqvt_at_def)
 apply(perm_simp)
-apply(rule refl)
+apply(simp)
+apply(simp add: perm_supp_eq)
 done
 
 termination (eqvt) by lexicographic_order
@@ -172,7 +165,6 @@
 | "(App t1 t2)[y ::== s] = App (t1[y ::== s]) (t2[y ::== s])"
 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::== s] = Lam [x].(t[y ::== (App (Var y) s)])"
   apply(simp add: eqvt_def subst'_graph_def)
-  apply(perm_simp, simp)
   apply(rule TrueI)
   apply(case_tac x)
   apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
@@ -182,8 +174,14 @@
   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
   apply(simp_all add: Abs_fresh_iff)
   apply(simp add: fresh_star_def fresh_Pair)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
 done
 
 termination (eqvt) by lexicographic_order
@@ -201,7 +199,7 @@
 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)"
   unfolding eqvt_def
   unfolding frees_lst_graph_def
-  apply (rule, perm_simp, rule)
+apply(simp)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)
@@ -227,7 +225,6 @@
 | "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2"
 | "frees_set (Lam [x]. t) = (frees_set t) - {atom x}"
   apply(simp add: eqvt_def frees_set_graph_def)
-  apply(rule, perm_simp, rule)
   apply(erule frees_set_graph.induct)
   apply(auto)[9]
   apply(rule_tac y="x" in lam.exhaust)
@@ -236,8 +233,8 @@
   apply(erule_tac c="()" in Abs_lst1_fcb2)
   apply(simp add: fresh_minus_atom_set)
   apply(simp add: fresh_star_def fresh_Unit)
-  apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl)
-  apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl)
+  apply(simp add: Diff_eqvt eqvt_at_def)
+  apply(simp add: Diff_eqvt eqvt_at_def)
   done
 
 termination (eqvt) 
@@ -255,7 +252,6 @@
 | "height (App t1 t2) = max (height t1) (height t2) + 1"
 | "height (Lam [x].t) = height t + 1"
   apply(simp add: eqvt_def height_graph_def)
-  apply (rule, perm_simp, rule)
   apply(rule TrueI)
   apply(rule_tac y="x" in lam.exhaust)
   apply(auto)
@@ -278,7 +274,7 @@
 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
   unfolding eqvt_def subst_graph_def
-  apply (rule, perm_simp, rule)
+  apply(simp)
   apply(rule TrueI)
   apply(auto)
   apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
@@ -287,8 +283,14 @@
   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
   apply(simp_all add: Abs_fresh_iff)
   apply(simp add: fresh_star_def fresh_Pair)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
 done
 
 termination (eqvt)
@@ -457,7 +459,6 @@
 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"
 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))"
   apply (simp add: eqvt_def trans_graph_def)
-  apply (rule, perm_simp, rule)
   apply (erule trans_graph.induct)
   apply (auto simp add: ln.fresh)[3]
   apply (simp add: supp_lookup_fresh)
@@ -471,8 +472,12 @@
   apply (erule_tac c="xsa" in Abs_lst1_fcb2')
   apply (simp add: fresh_star_def)
   apply (simp add: fresh_star_def)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
   done
 
 termination (eqvt)
@@ -488,7 +493,6 @@
 | "cntlams (App t1 t2) = (cntlams t1) + (cntlams t2)"
 | "cntlams (Lam [x]. t) = Suc (cntlams t)"
   apply(simp add: eqvt_def cntlams_graph_def)
-  apply(rule, perm_simp, rule)
   apply(rule TrueI)
   apply(rule_tac y="x" in lam.exhaust)
   apply(auto)[3]
@@ -515,7 +519,6 @@
 | "cntbvs (App t1 t2) xs = (cntbvs t1 xs) + (cntbvs t2 xs)"
 | "atom x \<sharp> xs \<Longrightarrow> cntbvs (Lam [x]. t) xs = cntbvs t (x # xs)"
   apply(simp add: eqvt_def cntbvs_graph_def)
-  apply(rule, perm_simp, rule)
   apply(rule TrueI)
   apply(case_tac x)
   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
@@ -528,8 +531,12 @@
   apply(erule Abs_lst1_fcb2')
   apply(simp add: pure_fresh fresh_star_def)
   apply(simp add: fresh_star_def)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
   done
 
 termination (eqvt)
@@ -570,7 +577,7 @@
       Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))"
 | "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))"
   unfolding eqvt_def transdb_graph_def
-  apply (rule, perm_simp, rule)
+  apply(simp)
   apply(rule TrueI)
   apply (case_tac x)
   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
@@ -580,7 +587,14 @@
   apply (erule_tac c="xsa" in Abs_lst1_fcb2')
   apply (simp add: pure_fresh)
   apply(simp add: fresh_star_def fresh_at_list)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq eqvts eqvts_raw)+
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
   done
 
 termination (eqvt)
@@ -624,7 +638,6 @@
 | "apply_subst (App t0 t1) t2 = App (App t0 t1) t2"
 | "atom x \<sharp> t2 \<Longrightarrow> apply_subst (Lam [x].t1) t2 = eval (t1[x::= t2])"
   apply(simp add: eval_apply_subst_graph_def eqvt_def)
-  apply(rule, perm_simp, rule)
   apply(rule TrueI)
   apply (case_tac x)
   apply (case_tac a rule: lam.exhaust)
@@ -648,8 +661,12 @@
   apply (simp add: finite_supp)
   apply (simp add: fresh_Inl var_fresh_subst)
   apply(simp add: fresh_star_def)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst.eqvt)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst.eqvt)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
 done
 
 
@@ -671,7 +688,7 @@
 | "q (Var x) N = Var x"
 | "q (App l r) N = App l r"
 unfolding eqvt_def q_graph_def
-apply (rule, perm_simp, rule)
+apply (simp)
 apply (rule TrueI)
 apply (case_tac x)
 apply (rule_tac y="a" in lam.exhaust)
@@ -699,7 +716,6 @@
 | "eqvt f \<Longrightarrow> map_term f (Lam [x].t) = Lam [x].(f t)"
 | "\<not>eqvt f \<Longrightarrow> map_term f t = t"
   apply (simp add: eqvt_def map_term_graph_def)
-  apply (rule, perm_simp, rule)
   apply(rule TrueI)
   apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
   apply auto
@@ -819,7 +835,6 @@
 | "\<lbrakk>{atom x} \<sharp>* (s, xs); {atom y} \<sharp>* (t, xs); x \<noteq> y\<rbrakk> \<Longrightarrow> 
        aux (Lam [x].t) (Lam [y].s) xs = aux t s ((x, y) # xs)"
   apply (simp add: eqvt_def aux_graph_def)
-  apply (rule, perm_simp, rule)
   apply(erule aux_graph.induct)
   apply(simp_all add: fresh_star_def pure_fresh)[9]
   apply(case_tac x)
@@ -867,7 +882,7 @@
 | "aux2 (Lam [x].t) (App t1 t2) = False"
 | "x = y \<Longrightarrow> aux2 (Lam [x].t) (Lam [y].s) = aux2 t s"
   apply(simp add: eqvt_def aux2_graph_def)
-  apply(rule, perm_simp, rule, rule)
+  apply(simp)
   apply(case_tac x)
   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
   apply(rule_tac y="b" in lam.exhaust)

--- a/Nominal/Ex/Let.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Ex/Let.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -75,7 +75,6 @@
 apply(simp add: trm_assn.perm_bn_simps)
 apply(simp add: trm_assn.perm_bn_simps)
 apply(simp add: trm_assn.bn_defs)
-apply(simp add: atom_eqvt)
 done
 
 
@@ -95,11 +94,10 @@
 lemma [eqvt]:
   "p \<bullet> (apply_assn f a) = apply_assn (p \<bullet> f) (p \<bullet> a)"
   apply(induct f a rule: apply_assn.induct)
-  apply simp_all
+  apply simp
+  apply(simp only: apply_assn.simps trm_assn.perm_simps)
   apply(perm_simp)
-  apply rule
-  apply(perm_simp)
-  apply simp
+  apply(simp)
   done
 
 lemma alpha_bn_apply_assn:
@@ -155,8 +153,6 @@
   "p \<bullet> (apply_assn2 f a) = apply_assn2 (p \<bullet> f) (p \<bullet> a)"
   apply(induct f a rule: apply_assn2.induct)
   apply simp_all
-  apply(perm_simp)
-  apply rule
   done
 
 lemma bn_apply_assn2: "bn (apply_assn2 f as) = bn as"

--- a/Nominal/Ex/LetRec.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Ex/LetRec.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -46,8 +46,10 @@
   apply (case_tac b rule: let_rec.exhaust(2))
   apply blast
   apply (erule Abs_set_fcb)
-  apply (simp_all add: pure_fresh)
-  apply (simp add: eqvt_at_def)
+  apply (simp_all add: pure_fresh)[2]
+  apply (simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp)
   apply (simp add: Abs_eq_iff2)
   apply (simp add: alphas)
   apply clarify
@@ -55,8 +57,6 @@
   apply(rule_tac p="p" in supp_perm_eq[symmetric])
   apply (simp add: pure_supp fresh_star_def)
   apply(simp add: eqvt_at_def)
-  apply(perm_simp)
-  apply (simp add: permute_fun_def)
   done
 
 termination (eqvt) by lexicographic_order

--- a/Nominal/Ex/Pi.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Ex/Pi.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -35,11 +35,11 @@
   apply(auto)
   apply(subgoal_tac "\<And>p x r. subst_name_list_graph x r \<Longrightarrow> subst_name_list_graph (p \<bullet> x) (p \<bullet> r)")
   unfolding eqvt_def
+  apply(simp only: permute_fun_def)
   apply(rule allI)
-  apply(simp add: permute_fun_def)
   apply(rule ext)
   apply(rule ext)
-  apply(simp add: permute_bool_def)
+  apply(simp only: permute_bool_def)
   apply(rule iffI)
   apply(drule_tac x="p" in meta_spec)
   apply(drule_tac x="- p \<bullet> x" in meta_spec)
@@ -183,10 +183,10 @@
   apply(subgoal_tac "\<And>p x r. subsGuard_mix_subsList_mix_subs_mix_graph x r \<Longrightarrow> subsGuard_mix_subsList_mix_subs_mix_graph (p \<bullet> x) (p \<bullet> r)")
   unfolding eqvt_def
   apply(rule allI)
-  apply(simp add: permute_fun_def)
+  apply(simp only: permute_fun_def)
   apply(rule ext)
   apply(rule ext)
-  apply(simp add: permute_bool_def)
+  apply(simp only: permute_bool_def)
   apply(rule iffI)
   apply(drule_tac x="p" in meta_spec)
   apply(drule_tac x="- p \<bullet> x" in meta_spec)
@@ -303,13 +303,14 @@
   apply(simp)
   apply(blast)
   --"compatibility"
-  apply (simp add: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])
+  apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])
   apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)")
   apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))")
   apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))")
   prefer 2
-  apply (simp add: eqvt_at_def subs_mix_def)
+  apply (simp only: eqvt_at_def subs_mix_def)
   apply rule
+  apply(simp (no_asm))
   apply (subst testrr)
   apply (simp add: subsGuard_mix_subsList_mix_subs_mix_sumC_def)
   apply (simp add: THE_default_def)
@@ -389,7 +390,11 @@
   apply (subgoal_tac "atom ba \<sharp> (\<lambda>(a, x, y). subs_mix a x y) (P, xa, ya)")
   apply simp
   apply (erule fresh_eqvt_at)
-  apply (simp_all add: fresh_Pair finite_supp eqvts eqvt_at_def fresh_Pair swap_fresh_fresh)
+  apply(simp add: finite_supp)
+  apply(simp)
+  apply(simp add: eqvt_at_def)
+  apply(drule_tac x="(atom b \<rightleftharpoons> atom ba)" in spec)
+  apply(simp)
   done
 
 termination (eqvt)

--- a/Nominal/Ex/TypeSchemes1.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Ex/TypeSchemes1.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -146,6 +146,7 @@
   apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
   apply (simp add: alphas fresh_star_zero)
   apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> T)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset Xs \<longleftrightarrow> x \<in> atom ` fset Xsa")
+  apply(simp)
   apply blast
   apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> T)")
   apply (simp add: supp_Pair eqvts eqvts_raw)
@@ -271,8 +272,6 @@
 apply(drule_tac x="atom name" in bspec)
 apply(auto)[1]
 apply(simp add: fresh_def supp_perm)
-apply(perm_simp)
-apply(auto)
 done
 
 nominal_primrec

--- a/Nominal/Ex/TypeSchemes2.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Ex/TypeSchemes2.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -173,7 +173,7 @@
 apply (simp add: eqvts)
 apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
 apply (simp add: image_eqvt eqvts_raw eqvts)
-apply (simp add: fresh_star_permute_iff)
+apply (simp only: fresh_star_permute_iff)
 apply(perm_simp)
 apply(assumption)
 apply(simp (no_asm_use) only: eqvts)
@@ -186,7 +186,7 @@
 apply (simp add: eqvts)
 apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
 apply (simp add: image_eqvt eqvts_raw eqvts)
-apply (simp add: fresh_star_permute_iff)
+apply (simp only: fresh_star_permute_iff)
 apply(perm_simp)
 apply(assumption)
 apply(simp)
@@ -252,6 +252,7 @@
   apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
   apply (simp add: alphas fresh_star_zero)
   apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> T)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa")
+  apply(simp)
   apply blast
   apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> T)")
   apply (simp add: supp_Pair eqvts eqvts_raw)
@@ -263,8 +264,11 @@
   apply (simp add: fresh_star_def fresh_def)
   apply (simp (no_asm) only: supp_eqvt[symmetric] Pair_eqvt[symmetric])
   apply (subgoal_tac "p \<bullet> supp (subst \<theta>' T) \<subseteq> p \<bullet> supp (\<theta>', T)")
-  apply (erule subsetD)
-  apply (simp add: supp_eqvt)
+  apply (erule_tac subsetD)
+  apply(simp only: supp_eqvt)
+  apply(perm_simp)
+  apply(drule_tac x="p" in spec)
+  apply(simp)
   apply (metis permute_pure subset_eqvt)
   apply (rule perm_supp_eq)
   apply (simp add: fresh_def fresh_star_def)

--- a/Nominal/Nominal2_Abs.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Nominal2_Abs.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -249,7 +249,7 @@
   unfolding Diff_eqvt[symmetric]
   apply(erule_tac [!] exE)
   apply(rule_tac [!] x="p \<bullet> pa" in exI)
-  by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric])
+  by (auto simp only: fresh_star_permute_iff permute_eqvt[symmetric])
 
 
 section {* Strengthening the equivalence *}

--- a/Nominal/Nominal2_Base.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -799,6 +799,21 @@
  {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *}
  {* pushes permutations inside, raises an error if it cannot solve all permutations. *}
 
+simproc_setup perm_simproc ("p \<bullet> t") = {* fn _ => fn ss => fn ctrm =>
+  case term_of (Thm.dest_arg ctrm) of 
+    Free _ => NONE
+  | Var _ => NONE
+  | Const (@{const_name permute}, _) $ _ $ _ => NONE
+  | _ =>
+      let
+        val ctxt = Simplifier.the_context ss
+        val thm = Nominal_Permeq.eqvt_conv ctxt Nominal_Permeq.eqvt_strict_config ctrm
+          handle ERROR _ => Thm.reflexive ctrm
+      in
+        if Thm.is_reflexive thm then NONE else SOME(thm)
+      end
+*}
+
 
 subsubsection {* Equivariance for permutations and swapping *}
 
@@ -876,10 +891,6 @@
   shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"
   by (simp add: permute_fun_def permute_bool_def)
 
-lemma Let_eqvt [eqvt]:
-  shows "p \<bullet> Let x y = Let (p \<bullet> x) (p \<bullet> y)"
-  unfolding Let_def permute_fun_app_eq ..
-
 lemma True_eqvt [eqvt]:
   shows "p \<bullet> True = True"
   unfolding permute_bool_def ..
@@ -920,7 +931,7 @@
   assumes unique: "\<exists>!x. P x"
   shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))"
   apply(rule the1_equality [symmetric])
-  apply(simp add: ex1_eqvt2[symmetric])
+  apply(simp only: ex1_eqvt2[symmetric])
   apply(simp add: permute_bool_def unique)
   apply(simp add: permute_bool_def)
   apply(rule theI'[OF unique])
@@ -940,84 +951,76 @@
 
 lemma inter_eqvt [eqvt]:
   shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
-  unfolding Int_def
-  by (perm_simp) (rule refl)
+  unfolding Int_def by simp
 
 lemma Bex_eqvt [eqvt]:
   shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
-  unfolding Bex_def
-  by (perm_simp) (rule refl)
+  unfolding Bex_def by simp
 
 lemma Ball_eqvt [eqvt]:
   shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
-  unfolding Ball_def
-  by (perm_simp) (rule refl)
+  unfolding Ball_def by simp
 
 lemma image_eqvt [eqvt]:
   shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
-  unfolding image_def
-  by (perm_simp) (rule refl)
+  unfolding image_def by simp
 
 lemma Image_eqvt [eqvt]:
   shows "p \<bullet> (R `` A) = (p \<bullet> R) `` (p \<bullet> A)"
-  unfolding Image_def
-  by (perm_simp) (rule refl)
+  unfolding Image_def by simp
 
 lemma UNIV_eqvt [eqvt]:
   shows "p \<bullet> UNIV = UNIV"
-  unfolding UNIV_def
+  unfolding UNIV_def 
   by (perm_simp) (rule refl)
 
 lemma union_eqvt [eqvt]:
   shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
-  unfolding Un_def
-  by (perm_simp) (rule refl)
+  unfolding Un_def by simp
 
 lemma Diff_eqvt [eqvt]:
   fixes A B :: "'a::pt set"
   shows "p \<bullet> (A - B) = (p \<bullet> A) - (p \<bullet> B)"
-  unfolding set_diff_eq
-  by (perm_simp) (rule refl)
+  unfolding set_diff_eq by simp
 
 lemma Compl_eqvt [eqvt]:
   fixes A :: "'a::pt set"
   shows "p \<bullet> (- A) = - (p \<bullet> A)"
-  unfolding Compl_eq_Diff_UNIV
-  by (perm_simp) (rule refl)
+  unfolding Compl_eq_Diff_UNIV by simp
 
 lemma subset_eqvt [eqvt]:
   shows "p \<bullet> (S \<subseteq> T) \<longleftrightarrow> (p \<bullet> S) \<subseteq> (p \<bullet> T)"
-  unfolding subset_eq
-  by (perm_simp) (rule refl)
+  unfolding subset_eq by simp
 
 lemma psubset_eqvt [eqvt]:
   shows "p \<bullet> (S \<subset> T) \<longleftrightarrow> (p \<bullet> S) \<subset> (p \<bullet> T)"
-  unfolding psubset_eq
-  by (perm_simp) (rule refl)
+  unfolding psubset_eq by simp
 
 lemma vimage_eqvt [eqvt]:
   shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
-  unfolding vimage_def
-  by (perm_simp) (rule refl)
+  unfolding vimage_def by simp
 
 lemma Union_eqvt [eqvt]:
   shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
-  unfolding Union_eq 
-  by (perm_simp) (rule refl)
+  unfolding Union_eq by simp
 
 lemma Inter_eqvt [eqvt]:
   shows "p \<bullet> (\<Inter> S) = \<Inter> (p \<bullet> S)"
-  unfolding Inter_eq 
-  by (perm_simp) (rule refl)
+  unfolding Inter_eq by simp
+
+thm foldr.simps
 
 lemma foldr_eqvt[eqvt]:
-  "p \<bullet> foldr a b c = foldr (p \<bullet> a) (p \<bullet> b) (p \<bullet> c)"
-  apply (induct b)
-  apply simp_all
-  apply (perm_simp)
-  apply simp
+  "p \<bullet> foldr f xs = foldr (p \<bullet> f) (p \<bullet> xs)"
+  apply(induct xs)
+  apply(simp_all)
+  apply(perm_simp exclude: foldr)
+  apply(simp)
   done
 
+thm eqvts_raw
+
+
 (* FIXME: eqvt attribute *)
 lemma Sigma_eqvt:
   shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"
@@ -1090,12 +1093,12 @@
   fixes F::"('a \<Rightarrow> 'b) \<Rightarrow> ('a::pt \<Rightarrow> 'b::{inf_eqvt, le_eqvt})"
   shows "p \<bullet> (lfp F) = lfp (p \<bullet> F)"
 unfolding lfp_def
-by (perm_simp) (rule refl)
+by simp
 
 lemma finite_eqvt [eqvt]:
   shows "p \<bullet> finite A = finite (p \<bullet> A)"
 unfolding finite_def
-by (perm_simp) (rule refl)
+by simp
 
 
 subsubsection {* Equivariance for product operations *}
@@ -1111,7 +1114,7 @@
 lemma split_eqvt [eqvt]: 
   shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
   unfolding split_def
-  by (perm_simp) (rule refl)
+  by simp
 
 
 subsubsection {* Equivariance for list operations *}
@@ -1126,7 +1129,7 @@
 
 lemma map_eqvt [eqvt]: 
   shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"
-  by (induct xs) (simp_all, simp only: permute_fun_app_eq)
+  by (induct xs) (simp_all)
 
 lemma removeAll_eqvt [eqvt]:
   shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
@@ -1156,15 +1159,14 @@
 
 lemma option_map_eqvt[eqvt]:
   shows "p \<bullet> (Option.map f x) = Option.map (p \<bullet> f) (p \<bullet> x)"
-  by (cases x) (simp_all, simp add: permute_fun_app_eq)
+  by (cases x) (simp_all)
 
 
 subsubsection {* Equivariance for @{typ "'a fset"} *}
 
 lemma in_fset_eqvt [eqvt]:
   shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))"
-unfolding in_fset
-by (perm_simp) (simp)
+unfolding in_fset by simp
 
 lemma union_fset_eqvt [eqvt]:
   shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"
@@ -1174,7 +1176,6 @@
   shows "(p \<bullet> (S |\<inter>| T)) = ((p \<bullet> S) |\<inter>| (p \<bullet> T))"
   apply(descending)
   unfolding list_eq_def inter_list_def
-  apply(perm_simp)
   apply(simp)
   done
 
@@ -1182,7 +1183,6 @@
   shows "(p \<bullet> (S |\<subseteq>| T)) = ((p \<bullet> S) |\<subseteq>| (p \<bullet> T))"
   apply(descending)
   unfolding sub_list_def
-  apply(perm_simp)
   apply(simp)
   done
   
@@ -1254,14 +1254,11 @@
 
 lemma supp_eqvt [eqvt]:
   shows "p \<bullet> (supp x) = supp (p \<bullet> x)"
-  unfolding supp_def
-  by (perm_simp)
-     (simp only: permute_eqvt[symmetric])
+  unfolding supp_def by simp
 
 lemma fresh_eqvt [eqvt]:
   shows "p \<bullet> (a \<sharp> x) = (p \<bullet> a) \<sharp> (p \<bullet> x)"
-  unfolding fresh_def
-  by (perm_simp) (rule refl)
+  unfolding fresh_def by simp
 
 lemma fresh_permute_iff:
   shows "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> a \<sharp> x"
@@ -1751,7 +1748,7 @@
       using assms by (simp add: eqvt_at_def)
     also have "\<dots> = (p + q) \<bullet> (f x)" by simp
     also have "\<dots> = f ((p + q) \<bullet> x)"
-      using assms by (simp add: eqvt_at_def)
+      using assms by (simp only: eqvt_at_def)
     finally have "p \<bullet> (f (q \<bullet> x)) = f (p \<bullet> q \<bullet> x)" by simp } 
   then show "eqvt_at f (q \<bullet> x)" unfolding eqvt_at_def
     by simp
@@ -1978,7 +1975,7 @@
   shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
 proof -
   have eqvt: "eqvt (\<lambda>S. \<Union> supp ` S)" 
-    unfolding eqvt_def
+    unfolding eqvt_def 
     by (perm_simp) (simp)
   have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
     by (rule supp_finite_atom_set[symmetric]) (rule Union_of_finite_supp_sets[OF fin])
@@ -2334,9 +2331,7 @@
 
 lemma fresh_star_eqvt [eqvt]:
   shows "p \<bullet> (as \<sharp>* x) \<longleftrightarrow> (p \<bullet> as) \<sharp>* (p \<bullet> x)"
-unfolding fresh_star_def
-by (perm_simp) (rule refl)
-
+unfolding fresh_star_def by simp
 
 
 section {* Induction principle for permutations *}
@@ -2709,7 +2704,8 @@
 	apply(blast)
 	apply(simp)
 	done
-      then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by (simp add: supp_swap)
+      then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
+        unfolding supp_swap by auto
       moreover
       have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
 	using ** by (auto simp add: insert_eqvt)
@@ -2777,7 +2773,8 @@
 	apply(blast)
 	apply(simp)
 	done
-      then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)" by (simp add: supp_swap)
+      then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)" 
+        unfolding supp_swap by auto
       moreover
       have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" 
 	using ** by (auto simp add: insert_eqvt)
@@ -2961,7 +2958,7 @@
   fixes a::"'a::at_base"
   shows "atom (p \<bullet> a) \<sharp> p \<bullet> x \<longleftrightarrow> atom a \<sharp> x"
   unfolding atom_eqvt[symmetric]
-  by (simp add: fresh_permute_iff)
+  by (simp only: fresh_permute_iff)
 
 
 section {* Infrastructure for concrete atom types *}

--- a/Nominal/Nominal2_FCB.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Nominal2_FCB.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -182,14 +182,14 @@
   then have "q \<bullet> (as \<sharp>* f as x c)"
     by (simp add: permute_bool_def)
   then have "(q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c"
-    apply(simp add: fresh_star_eqvt set_eqvt)
+    apply(simp only: fresh_star_eqvt set_eqvt)
     apply(subst (asm) perm1)
     using inc fresh1 fr1
     apply(auto simp add: fresh_star_def fresh_Pair)
     done
   then have "(r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp
   then have "r \<bullet> (bs \<sharp>* f bs y c)"
-    apply(simp add: fresh_star_eqvt set_eqvt)
+    apply(simp only: fresh_star_eqvt set_eqvt)
     apply(subst (asm) perm2[symmetric])
     using qq3 fresh2 fr1
     apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)
@@ -264,7 +264,7 @@
   then have "q \<bullet> ((as \<inter> supp x) \<sharp>* f (as \<inter> supp x) x c)"
     by (simp add: permute_bool_def)
   then have "(q \<bullet> (as \<inter> supp x)) \<sharp>* f (q \<bullet> (as \<inter> supp x)) (q \<bullet> x) c"
-    apply(simp add: fresh_star_eqvt set_eqvt)
+    apply(simp only: fresh_star_eqvt set_eqvt)
     apply(subst (asm) perm1)
     using inc fresh1 fr1
     apply(auto simp add: fresh_star_def fresh_Pair)
@@ -274,7 +274,7 @@
     apply simp
     done
   then have "r \<bullet> ((bs \<inter> supp y) \<sharp>* f (bs \<inter> supp y) y c)"
-    apply(simp add: fresh_star_eqvt set_eqvt)
+    apply(simp only: fresh_star_eqvt set_eqvt)
     apply(subst (asm) perm2[symmetric])
     using qq3 fresh2 fr1
     apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)
@@ -350,14 +350,14 @@
   then have "q \<bullet> ((set as) \<sharp>* f as x c)"
     by (simp add: permute_bool_def)
   then have "set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c"
-    apply(simp add: fresh_star_eqvt set_eqvt)
+    apply(simp only: fresh_star_eqvt set_eqvt)
     apply(subst (asm) perm1)
     using inc fresh1 fr1
     apply(auto simp add: fresh_star_def fresh_Pair)
     done
   then have "set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp
   then have "r \<bullet> ((set bs) \<sharp>* f bs y c)"
-    apply(simp add: fresh_star_eqvt set_eqvt)
+    apply(simp only: fresh_star_eqvt set_eqvt)
     apply(subst (asm) perm2[symmetric])
     using qq3 fresh2 fr1
     apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)

--- a/Nominal/nominal_permeq.ML	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/nominal_permeq.ML	Mon Jun 04 21:39:51 2012 +0100
@@ -18,6 +18,7 @@
   val delpres : eqvt_config -> eqvt_config
   val delposts : eqvt_config -> eqvt_config
 
+  val eqvt_conv: Proof.context -> eqvt_config -> conv 
   val eqvt_rule: Proof.context -> eqvt_config -> thm -> thm
   val eqvt_tac: Proof.context -> eqvt_config -> int -> tactic
 

--- a/Tutorial/Lambda.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Tutorial/Lambda.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -39,7 +39,6 @@
 | "height (App t1 t2) = max (height t1) (height t2) + 1"
 | "height (Lam [x].t) = height t + 1"
 apply(simp add: eqvt_def height_graph_def)
-apply (rule, perm_simp, rule)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)
@@ -69,8 +68,10 @@
   apply(erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
   apply(simp_all add: Abs_fresh_iff)
   apply(simp add: fresh_star_def fresh_Pair)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
+  apply(simp add: perm_supp_eq fresh_star_Pair)
+  apply(simp add: eqvt_at_def)
+  apply(simp add: perm_supp_eq fresh_star_Pair)
 done
 
 termination (eqvt)
@@ -82,7 +83,7 @@
   shows "atom z \<sharp> t[y ::= s]"
 using a b
 by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
-   (auto simp add: lam.fresh fresh_at_base)
+   (auto simp add: fresh_at_base)
 
 
 end