diff -r 14f24be9e499 -r bff7a1466fe4 doc-src/IsarImplementation/Thy/document/integration.tex
--- a/doc-src/IsarImplementation/Thy/document/integration.tex	Tue Jan 03 11:57:33 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Tue Jan 03 13:59:55 2006 +0100
@@ -394,7 +394,7 @@
   been concluded, in order to support legacy proof {\ML} proof
   scripts.
 
-  The basic internal actions of the theory database are \isa{update}\indexbold{\isa{update} theory}, \isa{outdate}\indexbold{\isa{outdate} theory}, and \isa{remove}\indexbold{\isa{remove} theory}:
+  The basic internal actions of the theory database are \isa{update}, \isa{outdate}, and \isa{remove}:
 
   \begin{itemize}