
diff -r 14f24be9e499 -r bff7a1466fe4 doc-src/IsarImplementation/Thy/integration.thy
--- a/doc-src/IsarImplementation/Thy/integration.thy	Tue Jan 03 11:57:33 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/integration.thy	Tue Jan 03 13:59:55 2006 +0100
@@ -321,9 +321,7 @@
   scripts.
 
   The basic internal actions of the theory database are @{text
-  "update"}\indexbold{@{text "update"} theory}, @{text
-  "outdate"}\indexbold{@{text "outdate"} theory}, and @{text
-  "remove"}\indexbold{@{text "remove"} theory}:
+  "update"}, @{text "outdate"}, and @{text "remove"}:
 
   \begin{itemize}
 




