diff -r 9cb98d34f593 -r e88e980ed735 src/HOL/MicroJava/BV/JVM.thy
--- a/src/HOL/MicroJava/BV/JVM.thy	Sun Jan 15 14:55:30 2012 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Sun Jan 15 18:55:27 2012 +0100
@@ -112,11 +112,11 @@
   from phi' have l: "size phi' = size bs" by simp  
   with instrs w have "phi' ! 0 \<noteq> Err" by (unfold wt_step_def) simp
   with instrs l have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0"
-    by (clarsimp simp add: not_Err_eq)  
+    by auto
 
   from phi' have "check_types G maxs maxr phi'" by(simp add: check_types_def)
   also from w have "phi' = map OK (map ok_val phi')" 
-    by (auto simp add: wt_step_def not_Err_eq intro!: nth_equalityI)
+    by (auto simp add: wt_step_def intro!: nth_equalityI)
   finally 
   have check_types:
     "check_types G maxs maxr (map OK (map ok_val phi'))" .