diff -r f97643a56615 -r d8bbb97689d3 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Aug 07 12:17:41 2014 +0200
@@ -1392,7 +1392,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 list.set list.map) apply blast
   apply (simp (no_asm_simp))
   apply simp                    (* subgoal bc3 = [] *)
   apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> sttp2 = sttp3 *)
@@ -1419,7 +1419,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 list.set list.map) apply blast
   apply (simp (no_asm_simp))
 
 apply (drule_tac x=sttp2 in spec, simp) (* subgoal \<exists>mt3_rest. \<dots> *)