# HG changeset patch
# User wenzelm
# Date 1180648058 -7200
# Node ID 8db2b22257bd9232cfa731f9cb8374d0030841de
# Parent  07ba6b58b3d2f75a84191df181721f3a835bed3c
insert: canonical argument order;

diff -r 07ba6b58b3d2 -r 8db2b22257bd src/Pure/General/heap.ML
--- a/src/Pure/General/heap.ML	Thu May 31 23:47:36 2007 +0200
+++ b/src/Pure/General/heap.ML	Thu May 31 23:47:38 2007 +0200
@@ -14,7 +14,7 @@
   val empty: T
   val is_empty: T -> bool
   val merge: T * T -> T
-  val insert: elem * T -> T
+  val insert: elem -> T -> T
   val min: T -> elem        (*exception Empty*)
   val delete_min: T -> T    (*exception Empty*)
 end;
@@ -57,7 +57,7 @@
         GREATER => heap x2 a2 (merge (h1, b2))
       | _ => heap x1 a1 (merge (b1, h2)));
 
-fun insert (x, h) = merge (Heap (1, x, Empty, Empty), h);
+fun insert x h = merge (Heap (1, x, Empty, Empty), h);
 
 end;