diff -r 980d4194a212 -r b48ab741683b doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Feb 27 22:52:25 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Feb 27 23:13:01 2010 +0100
@@ -436,14 +436,14 @@
     val empty = [];
     val extend = I;
     fun merge (ts1, ts2) =
-      OrdList.union TermOrd.fast_term_ord ts1 ts2;
+      OrdList.union Term_Ord.fast_term_ord ts1 ts2;
   )
 
   val get = Terms.get;
 
   fun add raw_t thy =
     let val t = Sign.cert_term thy raw_t
-    in Terms.map (OrdList.insert TermOrd.fast_term_ord t) thy end;
+    in Terms.map (OrdList.insert Term_Ord.fast_term_ord t) thy end;
 
   end;
 *}