src/HOL/MicroJava/J/Eval.thy

--- a/src/HOL/MicroJava/J/Eval.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -226,7 +226,7 @@
   next
     case (Call a b c d e f g h i j k l m n o p q r s t u v s4)
     with Call_code show ?thesis
-      by(cases "s4")(simp, (erule meta_allE meta_impE|rule conjI refl| assumption)+)
+      by(cases "s4") auto
   qed(erule (3) that[OF refl]|assumption)+
 next
   case evals