insert: canonical argument order;
authorwenzelm
Thu May 31 23:47:38 2007 +0200 (2007-05-31 ago)
changeset 231798db2b22257bd
parent 23178 07ba6b58b3d2
child 23180 80b9caed2ba8
insert: canonical argument order;
src/Pure/General/heap.ML
     1.1 --- a/src/Pure/General/heap.ML	Thu May 31 23:47:36 2007 +0200
     1.2 +++ b/src/Pure/General/heap.ML	Thu May 31 23:47:38 2007 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4    val empty: T
     1.5    val is_empty: T -> bool
     1.6    val merge: T * T -> T
     1.7 -  val insert: elem * T -> T
     1.8 +  val insert: elem -> T -> T
     1.9    val min: T -> elem        (*exception Empty*)
    1.10    val delete_min: T -> T    (*exception Empty*)
    1.11  end;
    1.12 @@ -57,7 +57,7 @@
    1.13          GREATER => heap x2 a2 (merge (h1, b2))
    1.14        | _ => heap x1 a1 (merge (b1, h2)));
    1.15  
    1.16 -fun insert (x, h) = merge (Heap (1, x, Empty, Empty), h);
    1.17 +fun insert x h = merge (Heap (1, x, Empty, Empty), h);
    1.18  
    1.19  end;
    1.20