the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive

--- a/src/HOL/Nominal/Examples/Compile.thy	Wed Mar 28 17:27:44 2007 +0200
+++ b/src/HOL/Nominal/Examples/Compile.thy	Wed Mar 28 18:25:23 2007 +0200
@@ -130,7 +130,7 @@
   and   x::"name"
   shows "pi\<bullet>(t1[x::=t2]) = ((pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)])"
   apply (nominal_induct t1 avoiding: x t2 rule: trmI.induct)
-  apply (simp_all add: Isubst.simps eqvt fresh_bij)
+  apply (simp_all add: Isubst.simps eqvts fresh_bij)
   done
 
 lemma Isubst_supp:

--- a/src/HOL/Nominal/Examples/Fsub.thy	Wed Mar 28 17:27:44 2007 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Wed Mar 28 18:25:23 2007 +0200
@@ -92,7 +92,7 @@
   and   pi'::"vrs prm"
   shows "pi\<bullet>(domain \<Gamma>) = domain (pi\<bullet>\<Gamma>)"
   and   "pi'\<bullet>(domain \<Gamma>) = domain (pi'\<bullet>\<Gamma>)"
-  by (induct \<Gamma>) (simp_all add: eqvt)
+  by (induct \<Gamma>) (simp_all add: eqvts)
 
 lemma finite_domain:
   shows "finite (domain \<Gamma>)"

--- a/src/HOL/Nominal/Examples/SN.thy	Wed Mar 28 17:27:44 2007 +0200
+++ b/src/HOL/Nominal/Examples/SN.thy	Wed Mar 28 18:25:23 2007 +0200
@@ -93,7 +93,7 @@
 apply(rule conjI)
 apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] calc_atm)
 apply(force dest!: supp_beta simp add: fresh_def)
-apply(force intro!: eqvt)
+apply(force intro!: eqvts)
 done
 
 lemma beta_subst: 

--- a/src/HOL/Nominal/Examples/SOS.thy	Wed Mar 28 17:27:44 2007 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Wed Mar 28 18:25:23 2007 +0200
@@ -544,7 +544,7 @@
   apply(drule_tac pi="[(xa,x)]" in big_eqvt)
   apply(drule_tac pi="[(xa,x)]" in big_eqvt)
   apply(drule_tac pi="[(xa,x)]" in big_eqvt)
-  apply(perm_simp add: calc_atm eqvt)
+  apply(perm_simp add: calc_atm eqvts)
   done
 
 lemma  b_CaseL_elim[elim]: 
@@ -564,7 +564,7 @@
   apply(perm_simp add: fresh_prod)
   apply(drule meta_mp)
   apply(rule_tac pi="[(x\<^isub>1,x\<^isub>1')]" in big_eqvt')
-  apply(perm_simp add: eqvt calc_atm)
+  apply(perm_simp add: eqvts calc_atm)
   apply(assumption)
   apply(drule_tac x="[(x\<^isub>1,x\<^isub>1')]\<bullet>e'" in meta_spec)
   apply(drule meta_mp)
@@ -572,7 +572,7 @@
   apply(perm_simp add: fresh_prod)
   apply(drule meta_mp)
   apply(rule_tac pi="[(x\<^isub>1,x\<^isub>1')]" in big_eqvt')
-  apply(perm_simp add: eqvt calc_atm)
+  apply(perm_simp add: eqvts calc_atm)
   apply(assumption)
 done
 
@@ -593,7 +593,7 @@
   apply(perm_simp add: fresh_prod)
   apply(drule meta_mp)
   apply(rule_tac pi="[(x\<^isub>2,x\<^isub>2')]" in big_eqvt')
-  apply(perm_simp add: eqvt calc_atm)
+  apply(perm_simp add: eqvts calc_atm)
   apply(assumption)
   apply(drule_tac x="[(x\<^isub>2,x\<^isub>2')]\<bullet>e'" in meta_spec)
   apply(drule meta_mp)
@@ -601,7 +601,7 @@
   apply(perm_simp add: fresh_prod)
   apply(drule meta_mp)
   apply(rule_tac pi="[(x\<^isub>2,x\<^isub>2')]" in big_eqvt')
-  apply(perm_simp add: eqvt calc_atm)
+  apply(perm_simp add: eqvts calc_atm)
   apply(assumption)
 done
 
@@ -854,7 +854,7 @@
 apply(rule_tac x="pi\<bullet>v'" in exI)
 apply(auto)
 apply(drule_tac pi="pi" in big_eqvt)
-apply(perm_simp add: eqvt)
+apply(perm_simp add: eqvts)
 done
 
 lemma V_arrow_elim_weak[elim] :
@@ -887,7 +887,7 @@
 apply(rule_tac x="[(a,a')]\<bullet>v'" in exI)
 apply(auto)
 apply(drule_tac pi="[(a,a')]" in big_eqvt)
-apply(perm_simp add: eqvt calc_atm)
+apply(perm_simp add: eqvts calc_atm)
 apply(simp add: V_eqvt)
 (*A*)
 apply(rule exists_fresh')

--- a/src/HOL/Nominal/nominal_permeq.ML	Wed Mar 28 17:27:44 2007 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Mar 28 18:25:23 2007 +0200
@@ -151,7 +151,7 @@
 
 (* general simplification of permutations and permutation that arose from eqvt-problems *)
 val perm_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp"];
-val eqvt_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_pi_simp","eqvt"];
+val eqvt_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_pi_simp","eqvts"];
 
 (* main simplification tactics for permutations *)
 (* FIXME: perm_simp_tac should simplify more permutations *)

--- a/src/HOL/Nominal/nominal_thmdecls.ML	Wed Mar 28 17:27:44 2007 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Wed Mar 28 18:25:23 2007 +0200
@@ -30,10 +30,10 @@
 structure Data = GenericDataFun
 (
   val name = "HOL/Nominal/eqvt";
-  type T = {eqvt:thm list, fresh:thm list, bij:thm list};
-  val empty = ({eqvt=[], fresh=[], bij=[]}:T);
+  type T = {eqvts:thm list, fresh:thm list, bij:thm list};
+  val empty = ({eqvts=[], fresh=[], bij=[]}:T);
   val extend = I;
-  fun merge _ (r1:T,r2:T) = {eqvt  = Drule.merge_rules (#eqvt r1, #eqvt r2), 
+  fun merge _ (r1:T,r2:T) = {eqvts  = Drule.merge_rules (#eqvts r1, #eqvts r2), 
                              fresh = Drule.merge_rules (#fresh r1, #fresh r2), 
                              bij   = Drule.merge_rules (#bij r1, #bij r2)}
   fun print context (data:T) =
@@ -42,7 +42,7 @@
          Pretty.writeln (Pretty.big_list msg
            (map (ProofContext.pretty_thm (Context.proof_of context)) thms))
     in
-      (print_aux "Equivariance lemmas: " (#eqvt data);
+      (print_aux "Equivariance lemmas: " (#eqvts data);
        print_aux "Freshness lemmas: " (#fresh data);
        print_aux "Bijection lemmas: " (#bij data))
     end;
@@ -61,7 +61,7 @@
 exception EQVT_FORM of string;
 
 val print_data = Data.print o Context.Proof;
-val get_eqvt_thms = Context.Theory #> Data.get #> #eqvt;
+val get_eqvt_thms = Context.Theory #> Data.get #> #eqvts;
 val get_fresh_thms = Context.Theory #> Data.get #> #fresh;
 val get_bij_thms = Context.Theory #> Data.get #> #bij;
 
@@ -111,7 +111,7 @@
   let 
      val context' = fold (fn thm => Data.map (flag thm)) thms context 
   in 
-    Context.mapping (snd o PureThy.add_thmss [(("eqvt",(#eqvt (Data.get context'))),[])]) I context'
+    Context.mapping (snd o PureThy.add_thmss [(("eqvts",(#eqvts (Data.get context'))),[])]) I context'
   end;
 
 (* replaces every variable x in t with pi o x *) 
@@ -197,11 +197,11 @@
 
 fun bij_add_del_aux f   = simple_add_del_aux #bij "bij" f
 fun fresh_add_del_aux f = simple_add_del_aux #fresh "fresh" f
-fun eqvt_force_add_del_aux f = simple_add_del_aux #eqvt "eqvt" f
+fun eqvt_force_add_del_aux f = simple_add_del_aux #eqvts "eqvts" f
 
-fun eqvt_map f th (r:Data.T)  = {eqvt = (f th (#eqvt r)), fresh = #fresh r, bij = #bij r};
-fun fresh_map f th (r:Data.T) = {eqvt = #eqvt r, fresh = (f th (#fresh r)), bij = #bij r};
-fun bij_map f th (r:Data.T)   = {eqvt = #eqvt r, fresh = #fresh r, bij = (f th (#bij r))};
+fun eqvt_map f th (r:Data.T)  = {eqvts = (f th (#eqvts r)), fresh = #fresh r, bij = #bij r};
+fun fresh_map f th (r:Data.T) = {eqvts = #eqvts r, fresh = (f th (#fresh r)), bij = #bij r};
+fun bij_map f th (r:Data.T)   = {eqvts = #eqvts r, fresh = #fresh r, bij = (f th (#bij r))};
 
 val eqvt_add  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule)); 
 val eqvt_del  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule));