src/HOL/MicroJava/BV/JVMType.thy

--- a/src/HOL/MicroJava/BV/JVMType.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -258,7 +258,7 @@
     assume l: "length (l#ls) = length b"
     
     then obtain b' bs where b: "b = b'#bs"
-      by (cases b) (simp, simp add: neq_Nil_conv, rule that)
+      by (cases b) (simp, simp add: neq_Nil_conv)
 
     with f
     have "\<forall>n. n < length ls \<longrightarrow> (G \<turnstile> (ls!n) <=o (bs!n))"