diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/CTL/CTL.thy
--- a/doc-src/TutorialI/CTL/CTL.thy	Wed May 25 09:03:53 2005 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy	Wed May 25 09:04:24 2005 +0200
@@ -244,7 +244,7 @@
 automatically. This is what happens in the step case.
 
 The induction step is similar, but more involved, because now we face nested
-occurrences of @{const SOME}. As a result, @{text fast} is no longer able to
+occurrences of @{text SOME}. As a result, @{text fast} is no longer able to
 solve the subgoal and we apply @{thm[source]someI2_ex} by hand.  We merely
 show the proof commands but do not describe the details:
 *};