--- a/src/Doc/Codegen/Evaluation.thy Mon Jan 14 16:47:29 2019 +0100
+++ b/src/Doc/Codegen/Evaluation.thy Mon Jan 14 18:33:48 2019 +0000
@@ -197,7 +197,7 @@
code performing static evaluation (called a \<^emph>\<open>computation\<close>)
is compiled once and for all such that later calls do not
require any invocation of the code generator or the ML
- compiler at all. This topic deserved a dedicated chapter
+ compiler at all. This topic deserves a dedicated chapter
\secref{sec:computations}.
\<close>