diff -r cbc435f7b16b -r 9ec4482c9201 doc-src/IsarRef/Thy/HOLCF_Specific.thy
--- a/doc-src/IsarRef/Thy/HOLCF_Specific.thy	Thu Nov 13 21:43:46 2008 +0100
+++ b/doc-src/IsarRef/Thy/HOLCF_Specific.thy	Thu Nov 13 21:45:40 2008 +0100
@@ -10,7 +10,7 @@
 
 text {*
   \begin{matharray}{rcl}
-    @{command_def (HOLCF) "consts"} & : & \isartrans{theory}{theory} \\
+    @{command_def (HOLCF) "consts"} & : & @{text "theory \<rightarrow> theory"} \\
   \end{matharray}
 
   HOLCF provides a separate type for continuous functions @{text "\<alpha> \<rightarrow>
@@ -33,7 +33,7 @@
 
 text {*
   \begin{matharray}{rcl}
-    @{command_def (HOLCF) "domain"} & : & \isartrans{theory}{theory} \\
+    @{command_def (HOLCF) "domain"} & : & @{text "theory \<rightarrow> theory"} \\
   \end{matharray}
 
   \begin{rail}