--- 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