--- a/src/HOL/Docs/Main_Doc.thy Mon Mar 09 23:07:51 2009 +0100
+++ b/src/HOL/Docs/Main_Doc.thy Mon Mar 09 23:29:13 2009 +0100
@@ -541,7 +541,7 @@
\subsubsection*{Syntax}
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-@{text"empty"} & @{term"\<lambda>x. None"}\\
+@{term"Map.empty"} & @{term"\<lambda>x. None"}\\
@{term"m(x:=Some y)"} & @{term[source]"m(x:=Some y)"}\\
@{text"m(x\<^isub>1\<mapsto>y\<^isub>1,\<dots>,x\<^isub>n\<mapsto>y\<^isub>n)"} & @{text[source]"m(x\<^isub>1\<mapsto>y\<^isub>1)\<dots>(x\<^isub>n\<mapsto>y\<^isub>n)"}\\
@{term"map_upds m xs ys"} & @{term[source]"map_upds m xs ys"}\\