diff -r c33b542394f3 -r 8279a25ad0ae src/HOL/Nominal/Examples/CR.thy
--- a/src/HOL/Nominal/Examples/CR.thy	Wed Mar 28 18:25:23 2007 +0200
+++ b/src/HOL/Nominal/Examples/CR.thy	Wed Mar 28 19:16:11 2007 +0200
@@ -271,7 +271,7 @@
   apply(rule conjI)
   apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst])
   apply(simp add: calc_atm)
-  apply(force intro!: One_eqvt)
+  apply(force intro!: One.eqvt)
   done
 
 lemma one_app: 
@@ -314,7 +314,7 @@
   apply(simp add: subst_rename)
   (*A*)
   apply(force intro: one_fresh_preserv)
-  apply(force intro: One_eqvt)
+  apply(force intro: One.eqvt)
   done
 
 text {* first case in Lemma 3.2.4*}