src/HOL/MicroJava/Comp/LemmasComp.thy

 lemma max_spec_preserves_length:
   "max_spec G C (mn, pTs) = {((md,rT),pTs')} 
   \<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
 
 
 lemma ty_exprs_length [simp]: "(E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts)"
 apply (subgoal_tac "(E\<turnstile>e::T \<longrightarrow> True) \<and> (E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts) \<and> (E\<turnstile>s\<surd> \<longrightarrow> True)")