src/HOL/Product_Type.thy

--- a/src/HOL/Product_Type.thy	Thu May 24 17:05:30 2012 +0200
+++ b/src/HOL/Product_Type.thy	Thu May 24 17:25:53 2012 +0200
@@ -1028,7 +1028,10 @@
 by blast
 
 lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
-  by (auto, case_tac "f x", auto)
+  apply auto
+  apply (case_tac "f x")
+  apply auto
+  done
 
 lemma swap_inj_on:
   "inj_on (\<lambda>(i, j). (j, i)) A"