src/Doc/Main/Main_Doc.thy
changeset 55466 786edc984c98
parent 54744 1e7f2d296e19
child 55518 1ddb2edf5ceb
--- 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}