diff -r 42671298f037 -r 313a24b66a8d doc-src/IsarImplementation/Thy/document/Base.tex
--- a/doc-src/IsarImplementation/Thy/document/Base.tex	Sun Nov 07 23:32:26 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Base.tex	Mon Nov 08 00:00:47 2010 +0100
@@ -10,7 +10,7 @@
 \isacommand{theory}\isamarkupfalse%
 \ Base\isanewline
 \isakeyword{imports}\ Main\isanewline
-\isakeyword{uses}\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isacharslash}{\isachardot}{\isachardot}{\isacharslash}antiquote{\isacharunderscore}setup{\isachardot}ML{\isachardoublequoteclose}\isanewline
+\isakeyword{uses}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}antiquote{\isaliteral{5F}{\isacharunderscore}}setup{\isaliteral{2E}{\isachardot}}ML{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \isakeyword{begin}\isanewline
 \isanewline
 \isacommand{end}\isamarkupfalse%