diff -r 9429e7b5b827 -r f41ef840f09d src/HOL/MicroJava/Comp/LemmasComp.thy
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Sun Feb 16 21:33:28 2014 +0100
@@ -392,7 +392,7 @@
   \<Longrightarrow> length pTs = length pTs'"
 apply (frule max_spec2mheads)
 apply (erule exE)+
-apply (simp add: list_all2_def)
+apply (simp add: list_all2_iff)
 done