--- a/Nominal/Ex/Classical.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/Ex/Classical.thy	Tue May 11 18:20:25 2010 +0200
@@ -68,8 +68,6 @@
 
 thm alpha.intros
 
-declare permute_trm_raw.simps[eqvt]
-
 equivariance alpha
 equivariance alpha_trm_raw
 thm eqvts_raw

--- a/Nominal/Ex/CoreHaskell.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/Ex/CoreHaskell.thy	Tue May 11 18:20:25 2010 +0200
@@ -652,8 +652,6 @@
 thm eqvts
 thm eqvts_raw
 
-declare permute_tkind_raw_permute_ckind_raw_permute_ty_raw_permute_ty_lst_raw_permute_co_raw_permute_co_lst_raw_permute_trm_raw_permute_assoc_lst_raw_permute_pat_raw_permute_vars_raw_permute_tvars_raw_permute_cvars_raw.simps[eqvt]
-
 equivariance alpha_tkind_raw
 
 thm eqvts

--- a/Nominal/Ex/Ex1rec.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/Ex/Ex1rec.thy	Tue May 11 18:20:25 2010 +0200
@@ -30,8 +30,6 @@
 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
 thm lam_bp.fv[simplified lam_bp.supp(1-2)]
 
-declare permute_lam_raw_permute_bp_raw.simps[eqvt]
-
 equivariance alpha_lam_raw
 
 

--- a/Nominal/Ex/Ex2.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/Ex/Ex2.thy	Tue May 11 18:20:25 2010 +0200
@@ -27,8 +27,6 @@
 thm trm_pat.distinct
 thm trm_pat.fv[simplified trm_pat.supp(1-2)]
 
-declare permute_trm_raw_permute_pat_raw.simps[eqvt]
-
 equivariance alpha_trm_raw
 
 

--- a/Nominal/Ex/Ex3.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/Ex/Ex3.thy	Tue May 11 18:20:25 2010 +0200
@@ -31,8 +31,6 @@
 thm trm_pat.fv[simplified trm_pat.supp(1-2)]
 
 
-declare permute_trm_raw_permute_pat_raw.simps[eqvt]
-
 equivariance alpha_trm_raw
 
 

--- a/Nominal/Ex/ExLet.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/Ex/ExLet.thy	Tue May 11 18:20:25 2010 +0200
@@ -34,12 +34,7 @@
 (*thm trm_lts.supp*)
 thm trm_lts.fv[simplified trm_lts.supp(1-2)]
 
-
-declare permute_trm_raw_permute_lts_raw.simps[eqvt]
-
-equivariance alpha_trm_raw
-
-
+equivariance alpha_bn_raw
 
 primrec
   permute_bn_raw

--- a/Nominal/Ex/ExLetMult.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/Ex/ExLetMult.thy	Tue May 11 18:20:25 2010 +0200
@@ -22,8 +22,6 @@
 thm trm_lts.induct
 thm trm_lts.fv[simplified trm_lts.supp]
 
-declare permute_trm_raw_permute_lts_raw.simps[eqvt]
-
 equivariance alpha_trm_raw
 
 

--- a/Nominal/Ex/ExLetRec.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/Ex/ExLetRec.thy	Tue May 11 18:20:25 2010 +0200
@@ -32,8 +32,6 @@
 thm trm_lts.supp
 thm trm_lts.fv[simplified trm_lts.supp]
 
-declare permute_trm_raw_permute_lts_raw.simps[eqvt]
-
 equivariance alpha_trm_raw
 
 (* why is this not in HOL simpset? *)

--- a/Nominal/Ex/ExPS3.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/Ex/ExPS3.thy	Tue May 11 18:20:25 2010 +0200
@@ -35,8 +35,6 @@
 thm exp_pat.fv
 thm exp_pat.supp(1-2)
 
-declare permute_exp_raw_permute_pat_raw.simps[eqvt]
-
 equivariance alpha_exp_raw
 
 

--- a/Nominal/Ex/ExPS6.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/Ex/ExPS6.thy	Tue May 11 18:20:25 2010 +0200
@@ -32,8 +32,6 @@
 thm exp_pat.distinct
 thm exp_pat.supp
 
-declare permute_exp_raw_permute_pat_raw.simps[eqvt]
-
 equivariance alpha_exp_raw
 
 

--- a/Nominal/Ex/ExPS7.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/Ex/ExPS7.thy	Tue May 11 18:20:25 2010 +0200
@@ -28,8 +28,6 @@
 thm exp_lrb_lrbs.eq_iff
 thm exp_lrb_lrbs.supp
 
-declare permute_exp_raw_permute_lrb_raw_permute_lrbs_raw.simps[eqvt]
-
 equivariance alpha_exp_raw
 
 end

--- a/Nominal/Ex/ExPS8.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/Ex/ExPS8.thy	Tue May 11 18:20:25 2010 +0200
@@ -48,9 +48,6 @@
 thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv
 thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff
 
-
-declare permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[eqvt]
-
 equivariance alpha_exp_raw
 end
 

--- a/Nominal/Ex/LF.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/Ex/LF.thy	Tue May 11 18:20:25 2010 +0200
@@ -20,8 +20,6 @@
 
 thm kind_ty_trm.supp
 
-declare permute_kind_raw_permute_ty_raw_permute_trm_raw.simps[eqvt]
-
 equivariance alpha_trm_raw
 
 

--- a/Nominal/Ex/Lambda.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue May 11 18:20:25 2010 +0200
@@ -15,7 +15,6 @@
 
 declare lam.perm[eqvt]
 
-declare permute_lam_raw.simps[eqvt]
 equivariance alpha_lam_raw
 
 section {* Strong Induction Principles*}
@@ -259,7 +258,6 @@
 | a3: "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw' fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow>
    alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)"
 
-declare permute_lam_raw.simps[eqvt]
 equivariance alpha_lam_raw'
 
 thm eqvts_raw

--- a/Nominal/Ex/Modules.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/Ex/Modules.thy	Tue May 11 18:20:25 2010 +0200
@@ -68,8 +68,6 @@
 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)
 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv[simplified mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)]
 
-declare permute_mexp_raw_permute_body_raw_permute_defn_raw_permute_sexp_raw_permute_sbody_raw_permute_spec_raw_permute_ty_raw_permute_path_raw_permute_trm_raw.simps[eqvt]
-
 equivariance alpha_trm_raw
 
 

--- a/Nominal/Ex/SingleLet.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Tue May 11 18:20:25 2010 +0200
@@ -27,8 +27,6 @@
 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}
 thm trm_assg.fv[simplified trm_assg.supp(1-2)]
 
-declare permute_trm_raw_permute_assg_raw.simps[eqvt]
-
 equivariance alpha_trm_raw
 
 

--- a/Nominal/Ex/TestMorePerm.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/Ex/TestMorePerm.thy	Tue May 11 18:20:25 2010 +0200
@@ -26,7 +26,6 @@
 thm alpha_weird_raw.intros[no_vars]
 thm fv_weird_raw.simps[no_vars]
 
-declare permute_weird_raw.simps[eqvt]
 equivariance alpha_weird_raw
 
 

--- a/Nominal/Ex/TypeSchemes.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/Ex/TypeSchemes.thy	Tue May 11 18:20:25 2010 +0200
@@ -14,7 +14,6 @@
 
 lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp]
 
-declare permute_ty_raw_permute_tys_raw.simps[eqvt]
 equivariance alpha_ty_raw
 
 

--- a/Nominal/NewParser.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/NewParser.thy	Tue May 11 18:20:25 2010 +0200
@@ -395,7 +395,10 @@
   val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns;
   val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
   val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc
-  val thy = Local_Theory.exit_global lthy2;
+
+  val (_, lthy2a) = Local_Theory.note ((Binding.empty,
+    [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_def) lthy2;
+  val thy = Local_Theory.exit_global lthy2a;
   val thy_name = Context.theory_name thy
 
   val lthy3 = Theory_Target.init NONE thy;