--- a/src/Doc/Implementation/Logic.thy Sat Aug 15 19:42:35 2015 +0200
+++ b/src/Doc/Implementation/Logic.thy Sat Aug 15 20:07:05 2015 +0200
@@ -643,7 +643,7 @@
@{index_ML Thm.cterm_of: "Proof.context -> term -> cterm"} \\
@{index_ML Thm.apply: "cterm -> cterm -> cterm"} \\
@{index_ML Thm.lambda: "cterm -> cterm -> cterm"} \\
- @{index_ML Thm.all: "cterm -> cterm -> cterm"} \\
+ @{index_ML Thm.all: "Proof.context -> cterm -> cterm -> cterm"} \\
@{index_ML Drule.mk_implies: "cterm * cterm -> cterm"} \\
\end{mldecls}
\begin{mldecls}