--- a/src/HOL/Library/Stream.thy Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Library/Stream.thy Thu Feb 15 12:11:00 2018 +0100
@@ -457,7 +457,7 @@
lemma sset_flat[simp]: "\<forall>xs \<in> sset s. xs \<noteq> [] \<Longrightarrow>
sset (flat s) = (\<Union>xs \<in> sset s. set xs)" (is "?P \<Longrightarrow> ?L = ?R")
proof safe
- fix x assume ?P "x : ?L"
+ fix x assume ?P "x \<in> ?L"
then obtain m where "x = flat s !! m" by (metis image_iff sset_range)
with \<open>?P\<close> obtain n m' where "x = s !! n ! m'" "m' < length (s !! n)"
proof (atomize_elim, induct m arbitrary: s rule: less_induct)