--- a/src/Doc/Implementation/Prelim.thy Sat Jun 28 11:19:58 2014 +0200
+++ b/src/Doc/Implementation/Prelim.thy Sat Jun 28 15:34:43 2014 +0200
@@ -310,7 +310,7 @@
of the three kinds of contexts: theory, proof, generic.
\paragraph{Theory data} declarations need to implement the following
- SML signature:
+ ML signature:
\medskip
\begin{tabular}{ll}
@@ -336,7 +336,7 @@
chain of diamonds would cause an exponential blowup!
\paragraph{Proof context data} declarations need to implement the
- following SML signature:
+ following ML signature:
\medskip
\begin{tabular}{ll}