diff -r 51e026049e4d -r b6fe3b189725 doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Tue Oct 26 11:31:22 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Tue Oct 26 15:57:16 2010 +0200
@@ -519,7 +519,7 @@
   of this module do not care about the declaration order, since that
   data structure forces its own arrangement of elements.
 
-  Observe how the @{verbatim merge} operation joins the data slots of
+  Observe how the @{ML_text merge} operation joins the data slots of
   the two constituents: @{ML Ord_List.union} prevents duplication of
   common data from different branches, thus avoiding the danger of
   exponential blowup.  Plain list append etc.\ must never be used for