# HG changeset patch
# User wenzelm
# Date 1121263653 -7200
# Node ID 23b9c52612db7c14d5f80408990794a6da4bfb4c
# Parent  2406588f99cb1a030b3c92374cd4ddec25024a06
avoid excessive exceptions;

diff -r 2406588f99cb -r 23b9c52612db src/Pure/General/ord_list.ML
--- a/src/Pure/General/ord_list.ML	Wed Jul 13 16:07:32 2005 +0200
+++ b/src/Pure/General/ord_list.ML	Wed Jul 13 16:07:33 2005 +0200
@@ -24,32 +24,31 @@
 
 (* single elements *)
 
-exception ABSENT of int;
-
 fun find_index ord list x =
   let
-    fun find i [] = raise ABSENT i
+    fun find i [] = ~ i
       | find i (y :: ys) =
           (case ord (x, y) of
-            LESS => raise ABSENT i
+            LESS => ~ i
           | EQUAL => i
           | GREATER => find (i + 1) ys);
-  in find 0 list end;
+  in find 1 list end;
 
-fun member ord list x =
-  (find_index ord list x; true) handle ABSENT _ => false;
+fun member ord list x = find_index ord list x > 0;
 
 fun insert ord x list =
   let
-    fun insrt 0 ys = x :: ys
+    fun insrt 1 ys = x :: ys
       | insrt i (y :: ys) = y :: insrt (i - 1) ys;
-  in (find_index ord list x; list) handle ABSENT i => insrt i list end;
+    val idx = find_index ord list x;
+  in if idx > 0 then list else insrt (~ idx) list end;
 
 fun remove ord x list =
   let
-    fun rmove 0 (_ :: ys) = ys
+    fun rmove 1 (_ :: ys) = ys
       | rmove i (y :: ys) = y :: rmove (i - 1) ys;
-  in rmove (find_index ord list x) list handle ABSENT _ => list end;
+    val idx = find_index ord list x;
+  in if idx > 0 then rmove idx list else list end;
 
 
 (* lists as sets *)