diff -r 548a34929e98 -r 603320b93668 src/HOL/MicroJava/BV/JVM.thy
--- a/src/HOL/MicroJava/BV/JVM.thy	Thu Nov 12 17:21:43 2009 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Thu Nov 12 17:21:48 2009 +0100
@@ -117,11 +117,7 @@
 
   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')" 
-    apply (clarsimp simp add: wt_step_def not_Err_eq) 
-    apply (rule map_id [symmetric])
-    apply (erule allE, erule impE, assumption)
-    apply clarsimp
-    done    
+    by (auto simp add: wt_step_def not_Err_eq intro!: nth_equalityI)
   finally 
   have check_types:
     "check_types G maxs maxr (map OK (map ok_val phi'))" .