diff -r f8097de20576 -r 238c563bbe86 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri May 25 18:25:17 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri May 25 21:08:45 2007 +0200
@@ -464,7 +464,7 @@
        integer literals in target languages.
     \item[@{text "Pretty_Char"}] represents @{text HOL} characters by 
        character literals in target languages.
-    \item[@{text "Pretty_Char_chr"}] like @{text "Pretty_Char_chr"},
+    \item[@{text "Pretty_Char_chr"}] like @{text "Pretty_Char"},
        but also offers treatment of character codes; includes
        @{text "Pretty_Int"}.
     \item[@{text "ExecutableSet"}] allows to generate code