src/Pure/General/heap.ML

--- a/src/Pure/General/heap.ML	Wed Mar 17 14:00:45 2004 +0100
+++ b/src/Pure/General/heap.ML	Fri Mar 19 10:42:38 2004 +0100
@@ -56,7 +56,7 @@
   | merge (Empty, h) = h
   | merge (h1 as Heap (_, x1, a1, b1), h2 as Heap (_, x2, a2, b2)) =
       (case ord (x1, x2) of
-        Library.GREATER => heap x2 a2 (merge (h1, b2))
+        GREATER => heap x2 a2 (merge (h1, b2))
       | _ => heap x1 a1 (merge (b1, h2)));
 
 fun insert (x, h) = merge (Heap (1, x, Empty, Empty), h);