diff -r 824d3f1d8de6 -r 2080fe35abea doc-src/IsarImplementation/Thy/document/Logic.tex
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Tue May 03 20:59:24 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Tue May 03 21:07:24 2011 +0200
@@ -217,15 +217,15 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.class}{\mbox{\isa{class}}}}[]
 \rail@nont{\isa{nameref}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.sort}{\mbox{\isa{sort}}}}[]
 \rail@nont{\isa{sort}}[]
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@bar
 \rail@term{\hyperlink{ML antiquotation.type-name}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}name}}}}[]
 \rail@nextbar{1}
@@ -235,7 +235,7 @@
 \rail@endbar
 \rail@nont{\isa{nameref}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.typ}{\mbox{\isa{typ}}}}[]
 \rail@nont{\isa{type}}[]
 \rail@end
@@ -481,7 +481,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@term{\hyperlink{ML antiquotation.const-name}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}name}}}}[]
 \rail@nextbar{1}
@@ -489,7 +489,7 @@
 \rail@endbar
 \rail@nont{\isa{nameref}}[]
 \rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@term{\hyperlink{ML antiquotation.const}{\mbox{\isa{const}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -502,11 +502,11 @@
 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.term}{\mbox{\isa{term}}}}[]
 \rail@nont{\isa{term}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.prop}{\mbox{\isa{prop}}}}[]
 \rail@nont{\isa{prop}}[]
 \rail@end
@@ -813,27 +813,27 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.ctyp}{\mbox{\isa{ctyp}}}}[]
 \rail@nont{\isa{typ}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.cterm}{\mbox{\isa{cterm}}}}[]
 \rail@nont{\isa{term}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.cprop}{\mbox{\isa{cprop}}}}[]
 \rail@nont{\isa{prop}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.thm}{\mbox{\isa{thm}}}}[]
 \rail@nont{\isa{thmref}}[]
 \rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{ML antiquotation.thms}{\mbox{\isa{thms}}}}[]
 \rail@nont{\isa{thmrefs}}[]
 \rail@end
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
 \rail@term{\hyperlink{ML antiquotation.lemma}{\mbox{\isa{lemma}}}}[]
 \rail@bar
 \rail@nextbar{1}