
diff -r 61cd0ad6cd42 -r 9722171731af src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Mon Feb 27 20:42:09 2012 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy	Mon Feb 27 20:55:30 2012 +0100
@@ -217,10 +217,10 @@
   { 
     fix x 
     assume "length x = Suc 0"
-    hence "\<exists> l. x = [l]"  by - (cases x, auto)
+    hence "\<exists> l. x = [l]"  by (cases x) auto
   } note 0 = this
 
-  have "length a = Suc (Suc 0) \<Longrightarrow> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
+  have "length a = Suc (Suc 0) \<Longrightarrow> \<exists>l l'. a = [l,l']" by (cases a) (auto dest: 0)
   with * show ?thesis by (auto dest: 0)
 qed
 




