src/HOL/MicroJava/BV/JVM.thy

   apply (rule semilat_opt)
   apply (rule err_semilat_Product_esl)
   apply (rule err_semilat_upto_esl)
   apply (rule err_semilat_JType_esl, assumption+)
   apply (rule err_semilat_eslI)
-  apply (rule semilat_Listn_sl)
-  apply (rule err_semilat_JType_esl, assumption+)  
+  apply (rule Listn_sl)
+  apply (rule err_semilat_JType_esl, assumption+)
   done
 
 lemma sl_triple_conv:
   "JVMType.sl G maxs maxr == 
   (states G maxs maxr, JVMType.le G maxs maxr, JVMType.sup G maxs maxr)"