--- a/src/Doc/ProgProve/Bool_nat_list.thy Fri Feb 14 07:53:45 2014 +0100
+++ b/src/Doc/ProgProve/Bool_nat_list.thy Fri Feb 14 07:53:45 2014 +0100
@@ -394,8 +394,8 @@
and the \indexed{@{const map}}{map} function that applies a function to all elements of a list:
\begin{isabelle}
\isacom{fun} @{const map} @{text"::"} @{typ[source] "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"}\\
-@{text"\""}@{thm map.simps(1)}@{text"\" |"}\\
-@{text"\""}@{thm map.simps(2)}@{text"\""}
+@{text"\""}@{thm list.map(1)}@{text"\" |"}\\
+@{text"\""}@{thm list.map(2)}@{text"\""}
\end{isabelle}
\ifsem