--- a/src/Doc/Main/Main_Doc.thy Fri Feb 14 07:53:45 2014 +0100
+++ b/src/Doc/Main/Main_Doc.thy Fri Feb 14 07:53:46 2014 +0100
@@ -484,7 +484,7 @@
\begin{tabular}{@ {} l @ {~::~} l @ {}}
@{const Option.the} & @{typeof Option.the}\\
-@{const Option.map} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\
+@{const map_option} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\
@{const Option.set} & @{term_type_only Option.set "'a option \<Rightarrow> 'a set"}\\
@{const Option.bind} & @{term_type_only Option.bind "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"}
\end{tabular}