# HG changeset patch
# User wenzelm
# Date 1131550009 -3600
# Node ID 6450591da9f0c70c8fcad380d80f84f3b905954d
# Parent  1d403623dabc18728380364993af67478cb006b5
use existing exeption Empty;

diff -r 1d403623dabc -r 6450591da9f0 src/Pure/General/heap.ML
--- a/src/Pure/General/heap.ML	Wed Nov 09 16:26:48 2005 +0100
+++ b/src/Pure/General/heap.ML	Wed Nov 09 16:26:49 2005 +0100
@@ -15,9 +15,8 @@
   val is_empty: T -> bool
   val merge: T * T -> T
   val insert: elem * T -> T
-  exception EMPTY
-  val min: T -> elem        (*exception EMPTY*)
-  val delete_min: T -> T    (*exception EMPTY*)
+  val min: T -> elem        (*exception Empty*)
+  val delete_min: T -> T    (*exception Empty*)
 end;
 
 functor HeapFun(type elem val ord: elem * elem -> order): HEAP =
@@ -65,12 +64,10 @@
 
 (* minimum element *)
 
-exception EMPTY
-
-fun min Empty = raise EMPTY
+fun min Empty = raise List.Empty
   | min (Heap (_, x, _, _)) = x;
 
-fun delete_min Empty = raise EMPTY
+fun delete_min Empty = raise List.Empty
   | delete_min (Heap (_, _, a, b)) = merge (a, b);
 
 end;