diff -r ef1e0cb80fde -r 949d93804740 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Tue May 22 14:12:15 2018 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Tue May 22 11:08:37 2018 +0200
@@ -572,7 +572,6 @@
 @{term"[m..<n]"} & @{term[source]"upt m n"}\\
 @{term"[i..j]"} & @{term[source]"upto i j"}\\
 \<open>[e. x \<leftarrow> xs]\<close> & @{term"map (%x. e) xs"}\\
-@{term"[x \<leftarrow> xs. b]"} & @{term[source]"filter (\<lambda>x. b) xs"} \\
 @{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\
 @{term"\<Sum>x\<leftarrow>xs. e"} & @{term[source]"listsum (map (\<lambda>x. e) xs)"}\\
 \end{supertabular}