diff -r c93ae0eb9631 -r a6fb4ddc05c7 doc-src/TutorialI/Advanced/simp.thy
--- a/doc-src/TutorialI/Advanced/simp.thy	Mon May 02 08:17:16 2005 +0200
+++ b/doc-src/TutorialI/Advanced/simp.thy	Mon May 02 10:56:13 2005 +0200
@@ -140,7 +140,7 @@
 The simplifier will still try to apply the rule provided it
 matches directly: without much $\lambda$-calculus hocus
 pocus.  For example, @{text"(?f ?x \<in> range ?f) = True"} rewrites
-@{term"g a \<in> range g"} to @{term True}, but will fail to match
+@{term"g a \<in> range g"} to @{const True}, but will fail to match
 @{text"g(h b) \<in> range(\<lambda>x. g(h x))"}.  However, you can
 eliminate the offending subterms --- those that are not patterns ---
 by adding new variables and conditions.