--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Dec 25 17:39:07 2013 +0100
@@ -944,7 +944,7 @@
apply assumption+ apply (rule HOL.refl)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp) add: max_ssize_def)
- apply (simp add: max_of_list_def max_ac)
+ apply (simp add: max_of_list_def ac_simps)
apply arith
apply (simp (no_asm_simp))+
@@ -961,7 +961,7 @@
apply (subgoal_tac "((mt2 @ [Some sttp2]) ! length bc2) = Some sttp2")
apply (simp only:)
apply (rule check_type_mono) apply assumption
-apply (simp (no_asm_simp) add: max_ssize_def max_ac)
+apply (simp (no_asm_simp) add: max_ssize_def ac_simps)
apply (simp add: nth_append)
apply (erule conjE)+