--- 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