diff --git a/doc/whyml.tex b/doc/whyml.tex
index 5683455cbfd0f15fca3c3937666c25aa75e17d16..4da89e5afee572b44b82f9b3ab67b3fe0f2c3208 100644
--- a/doc/whyml.tex
+++ b/doc/whyml.tex
@@ -132,7 +132,7 @@ end
 We now start a new theory, \texttt{Einstein}, which will contain all
 the individuals of the problem.
 \begin{whycode}
-theory Einstein "Einstein's problem"
+theory Einstein
 \end{whycode}
 First, we introduce enumeration types for houses, colors, persons,
 drinks, cigars, and pets.
@@ -194,7 +194,7 @@ end
 The next theory contains the 15 hypotheses. It starts by importing
 theory \texttt{Einstein}.
 \begin{whycode}
-theory EinsteinHints "Hints"
+theory EinsteinHints
   use import Einstein
 \end{whycode}
 Then each hypothesis is stated in terms of \texttt{to\_} and \texttt{of}
@@ -214,7 +214,7 @@ end
 \end{whycode}
 Finally, we declare the goal in a fourth theory:
 \begin{whycode}
-theory Problem "Goal of Einstein's problem"
+theory Problem
   use import Einstein
   use import EinsteinHints