diff -r 8ea7403147c5 -r ff9d8a8932e4 doc-src/IsarRef/Thy/document/HOLCF_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex	Thu Nov 13 22:44:40 2008 +0100
+++ b/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex	Thu Nov 13 22:45:12 2008 +0100
@@ -30,7 +30,7 @@
 %
 \begin{isamarkuptext}%
 \begin{matharray}{rcl}
-    \indexdef{HOLCF}{command}{consts}\hypertarget{command.HOLCF.consts}{\hyperlink{command.HOLCF.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isartrans{theory}{theory} \\
+    \indexdef{HOLCF}{command}{consts}\hypertarget{command.HOLCF.consts}{\hyperlink{command.HOLCF.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   \end{matharray}
 
   HOLCF provides a separate type for continuous functions \isa{{\isachardoublequote}{\isasymalpha}\ {\isasymrightarrow}\ {\isasymbeta}{\isachardoublequote}}, with an explicit application operator \isa{{\isachardoublequote}f\ {\isasymcdot}\ x{\isachardoublequote}}.
@@ -53,7 +53,7 @@
 %
 \begin{isamarkuptext}%
 \begin{matharray}{rcl}
-    \indexdef{HOLCF}{command}{domain}\hypertarget{command.HOLCF.domain}{\hyperlink{command.HOLCF.domain}{\mbox{\isa{\isacommand{domain}}}}} & : & \isartrans{theory}{theory} \\
+    \indexdef{HOLCF}{command}{domain}\hypertarget{command.HOLCF.domain}{\hyperlink{command.HOLCF.domain}{\mbox{\isa{\isacommand{domain}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   \end{matharray}
 
   \begin{rail}