diff -r a0134252ac29 -r a879f14b6f95 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Feb 19 22:02:23 2014 +1100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Feb 19 16:32:37 2014 +0100
@@ -1394,7 +1394,7 @@
 
   apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append)
     apply (rule max_of_list_sublist)
-    apply (simp (no_asm_simp) only: set_append set.simps list.map) apply blast
+    apply (simp (no_asm_simp) only: set_append set_simps list.map) apply blast
   apply (simp (no_asm_simp))
   apply simp                    (* subgoal bc3 = [] *)
   apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> sttp2 = sttp3 *)
@@ -1421,7 +1421,7 @@
      (* (some) preconditions of  wt_instr_offset *)
   apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append)
   apply (rule max_of_list_sublist)
-    apply (simp (no_asm_simp) only: set_append set.simps list.map) apply blast
+    apply (simp (no_asm_simp) only: set_append set_simps list.map) apply blast
   apply (simp (no_asm_simp))
 
 apply (drule_tac x=sttp2 in spec, simp) (* subgoal \<exists>mt3_rest. \<dots> *)