diff -r de51a86fc903 -r cc97b347b301 src/HOL/Hoare_Parallel/RG_Examples.thy
--- a/src/HOL/Hoare_Parallel/RG_Examples.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -52,7 +52,7 @@
    apply force
   apply(erule le_less_trans2) 
   apply(case_tac t,simp+)
-  apply (simp add:add_commute)
+  apply (simp add:add.commute)
   apply(simp add: add_le_mono)
 apply(rule Basic)
    apply simp
@@ -61,7 +61,7 @@
     apply simp
    apply(erule le_less_trans2)
    apply(case_tac t,simp+)
-   apply (simp add:add_commute)
+   apply (simp add:add.commute)
    apply(rule add_le_mono, auto)
 done