src/HOL/Library/Sublist.thy

--- a/src/HOL/Library/Sublist.thy	Fri Apr 10 11:31:10 2015 +0200
+++ b/src/HOL/Library/Sublist.thy	Fri Apr 10 11:52:55 2015 +0200
@@ -144,7 +144,7 @@
 
 lemma take_prefix: "prefix xs ys \<Longrightarrow> prefix (take n xs) ys"
   apply (induct n arbitrary: xs ys)
-   apply (case_tac ys, simp_all)[1]
+   apply (case_tac ys; simp)
   apply (metis prefix_order.less_trans prefixI take_is_prefixeq)
   done