diff -r 9800a7602629 -r c6674504103f src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Tue Sep 25 10:27:43 2007 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Tue Sep 25 12:16:08 2007 +0200
@@ -118,7 +118,7 @@
 apply (rule exec_all_trans)
 apply (simp only: append_Nil)
 apply (drule_tac x="[]" in spec)
-apply (simp only: list.simps)
+apply (simp only: list.simps list.size)
 apply blast
 apply (rule exec_instr_in_exec_all)
 apply auto