diff -r 52cb0e965041 -r 9b4aec46ad78 doc-src/IsarRef/Thy/document/syntax.tex
--- a/doc-src/IsarRef/Thy/document/syntax.tex	Thu May 08 22:17:37 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/syntax.tex	Thu May 08 22:20:33 2008 +0200
@@ -510,16 +510,16 @@
     \indexdef{}{antiquotation}{abbrev}\mbox{\isa{abbrev}} & : & \isarantiq \\
     \indexdef{}{antiquotation}{typeof}\mbox{\isa{typeof}} & : & \isarantiq \\
     \indexdef{}{antiquotation}{typ}\mbox{\isa{typ}} & : & \isarantiq \\
-    \indexdef{}{antiquotation}{thm-style}\mbox{\isa{thm{\isacharunderscore}style}} & : & \isarantiq \\
-    \indexdef{}{antiquotation}{term-style}\mbox{\isa{term{\isacharunderscore}style}} & : & \isarantiq \\
+    \indexdef{}{antiquotation}{thm\_style}\mbox{\isa{thm{\isacharunderscore}style}} & : & \isarantiq \\
+    \indexdef{}{antiquotation}{term\_style}\mbox{\isa{term{\isacharunderscore}style}} & : & \isarantiq \\
     \indexdef{}{antiquotation}{text}\mbox{\isa{text}} & : & \isarantiq \\
     \indexdef{}{antiquotation}{goals}\mbox{\isa{goals}} & : & \isarantiq \\
     \indexdef{}{antiquotation}{subgoals}\mbox{\isa{subgoals}} & : & \isarantiq \\
     \indexdef{}{antiquotation}{prf}\mbox{\isa{prf}} & : & \isarantiq \\
-    \indexdef{}{antiquotation}{full-prf}\mbox{\isa{full{\isacharunderscore}prf}} & : & \isarantiq \\
+    \indexdef{}{antiquotation}{full\_prf}\mbox{\isa{full{\isacharunderscore}prf}} & : & \isarantiq \\
     \indexdef{}{antiquotation}{ML}\mbox{\isa{ML}} & : & \isarantiq \\
-    \indexdef{}{antiquotation}{ML-type}\mbox{\isa{ML{\isacharunderscore}type}} & : & \isarantiq \\
-    \indexdef{}{antiquotation}{ML-struct}\mbox{\isa{ML{\isacharunderscore}struct}} & : & \isarantiq \\
+    \indexdef{}{antiquotation}{ML\_type}\mbox{\isa{ML{\isacharunderscore}type}} & : & \isarantiq \\
+    \indexdef{}{antiquotation}{ML\_struct}\mbox{\isa{ML{\isacharunderscore}struct}} & : & \isarantiq \\
   \end{matharray}
 
   The text body of formal comments (see also \secref{sec:comments})
@@ -579,7 +579,7 @@
   \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints theorems
   \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}.  Note that attribute specifications
   may be included as well (see also \secref{sec:syn-att}); the
-  \indexref{}{attribute}{no-vars}\mbox{\isa{no{\isacharunderscore}vars}} rule (see \secref{sec:misc-meth-att}) would
+  \indexref{}{attribute}{no\_vars}\mbox{\isa{no{\isacharunderscore}vars}} rule (see \secref{sec:misc-meth-att}) would
   be particularly useful to suppress printing of schematic variables.
 
   \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}{\isachardoublequote}}] prints a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.