--- a/src/HOL/Library/Sublist.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Library/Sublist.thy Thu Feb 15 13:04:36 2018 +0100
@@ -298,7 +298,7 @@
(is "_ \<Longrightarrow> \<exists>ps. ?P L ps")
proof(induction "LEAST n. \<exists>xs \<in>L. n = length xs" arbitrary: L)
case 0
- have "[] : L" using "0.hyps" LeastI[of "\<lambda>n. \<exists>xs\<in>L. n = length xs"] \<open>L \<noteq> {}\<close>
+ have "[] \<in> L" using "0.hyps" LeastI[of "\<lambda>n. \<exists>xs\<in>L. n = length xs"] \<open>L \<noteq> {}\<close>
by auto
hence "?P L []" by(auto)
thus ?case ..