diff -r e4817fa0f6a1 -r c33b542394f3 src/HOL/Nominal/Examples/SOS.thy
--- 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')