diff -r 3343670206eb -r 008126f730a0 doc-src/IsarImplementation/Thy/Integration.thy
--- a/doc-src/IsarImplementation/Thy/Integration.thy	Thu Jan 28 22:19:27 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Integration.thy	Thu Jan 28 22:38:11 2010 +0100
@@ -400,7 +400,7 @@
   descendants from the theory database.
 
   \item @{ML ThyInfo.begin_theory} is the basic operation behind a
-  @{text \<THEORY>} header declaration.  This is {\ML} functions is
+  @{text \<THEORY>} header declaration.  This {\ML} function is
   normally not invoked directly.
 
   \item @{ML ThyInfo.end_theory} concludes the loading of a theory