diff -r de51a86fc903 -r cc97b347b301 src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -137,7 +137,7 @@
 apply (simp only: append_assoc)
 apply (erule thin_rl, erule thin_rl)
 apply (drule_tac x="pre @ instrs0" in spec)
-apply (simp add: add_assoc)
+apply (simp add: add.assoc)
 done
 
 lemma progression_refl: 
@@ -196,7 +196,7 @@
 apply simp
 apply (erule thin_rl, erule thin_rl)
 apply (drule_tac x="pre @ instr # instrs0" in spec)
-apply (simp add: add_assoc)
+apply (simp add: add.assoc)
 done