diff -r 383b0a1837a9 -r aecb5bf6f76f doc-src/TutorialI/Recdef/simplification.thy
--- a/doc-src/TutorialI/Recdef/simplification.thy	Mon Oct 09 17:40:47 2000 +0200
+++ b/doc-src/TutorialI/Recdef/simplification.thy	Mon Oct 09 19:20:55 2000 +0200
@@ -60,7 +60,7 @@
 may not be expressible by pattern matching.
 
 A very simple alternative is to replace @{text if} by @{text case}, which
-is also available for @{typ"bool"} but is not split automatically:
+is also available for @{typ bool} but is not split automatically:
 *}
 
 consts gcd2 :: "nat\<times>nat \<Rightarrow> nat";