# HG changeset patch
# User wenzelm
# Date 1265470354 -3600
# Node ID c3e3ac3ca0919ff4041a23a577eeb494deb986ff
# Parent  9e55e87434ff95e2dbe3ebafcdbded69482f285d
removed unused "boundary" of Table/Graph.get_first;

diff -r 9e55e87434ff -r c3e3ac3ca091 src/HOL/SMT/Tools/z3_proof_rules.ML
--- a/src/HOL/SMT/Tools/z3_proof_rules.ML	Sat Feb 06 15:51:22 2010 +0100
+++ b/src/HOL/SMT/Tools/z3_proof_rules.ML	Sat Feb 06 16:32:34 2010 +0100
@@ -83,7 +83,7 @@
 val rule_of_string = Symtab.lookup rule_names
 fun string_of_rule r =
   let fun fit (s, r') = if r = r' then SOME s else NONE 
-  in the (Symtab.get_first NONE fit rule_names) end
+  in the (Symtab.get_first fit rule_names) end
 
 
 (* proof representation *)
@@ -545,7 +545,7 @@
 
   fun derive conj t lits idx ptab =
     let
-      val (l, lit) = the (Termtab.get_first NONE (get_lit conj t) lits)
+      val (l, lit) = the (Termtab.get_first (get_lit conj t) lits)
       val ls = explode_thm conj false false [t] lit
       val lits' = fold (Termtab.update o ` prop_of) ls (Termtab.delete l lits)
       fun upd (Sequent {hyps, vars, thm}) =
@@ -1231,7 +1231,7 @@
       (case Termtab.lookup tab @{term False} of
         SOME rs => extract_lit thm rs
       | NONE =>
-          pairself (extract_lit thm) (the (Termtab.get_first NONE pnlits tab))
+          pairself (extract_lit thm) (the (Termtab.get_first pnlits tab))
           |> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule)))
     end
   val falseE_v = Thm.dest_arg (Thm.dest_arg (Thm.cprop_of @{thm FalseE}))
diff -r 9e55e87434ff -r c3e3ac3ca091 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Sat Feb 06 15:51:22 2010 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Sat Feb 06 16:32:34 2010 +0100
@@ -127,7 +127,7 @@
 val empty = make_queue Inttab.empty Task_Graph.empty;
 
 fun all_passive (Queue {jobs, ...}) =
-  Task_Graph.get_first NONE
+  Task_Graph.get_first
     ((fn Job _ => SOME () | Running _ => SOME () | Passive => NONE) o #2 o #1 o #2) jobs |> is_none;
 
 
@@ -204,7 +204,7 @@
           if is_ready deps group then SOME (task, group, rev list) else NONE
       | ready _ = NONE;
   in
-    (case Task_Graph.get_first NONE ready jobs of
+    (case Task_Graph.get_first ready jobs of
       NONE => (NONE, queue)
     | SOME (result as (task, _, _)) =>
         let val jobs' = set_job task (Running thread) jobs
diff -r 9e55e87434ff -r c3e3ac3ca091 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Sat Feb 06 15:51:22 2010 +0100
+++ b/src/Pure/General/graph.ML	Sat Feb 06 16:32:34 2010 +0100
@@ -15,8 +15,7 @@
   val is_empty: 'a T -> bool
   val keys: 'a T -> key list
   val dest: 'a T -> (key * key list) list
-  val get_first: key option -> (key * ('a * (key list * key list)) -> 'b option) ->
-    'a T -> 'b option
+  val get_first: (key * ('a * (key list * key list)) -> 'b option) -> 'a T -> 'b option
   val fold: (key * ('a * (key list * key list)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
   val minimals: 'a T -> key list
   val maximals: 'a T -> key list
@@ -89,7 +88,7 @@
 fun keys (Graph tab) = Table.keys tab;
 fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, succs)) (Table.dest tab);
 
-fun get_first b f (Graph tab) = Table.get_first b f tab;
+fun get_first f (Graph tab) = Table.get_first f tab;
 fun fold_graph f (Graph tab) = Table.fold f tab;
 
 fun minimals G = fold_graph (fn (m, (_, ([], _))) => cons m | _ => I) G [];
diff -r 9e55e87434ff -r c3e3ac3ca091 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Sat Feb 06 15:51:22 2010 +0100
+++ b/src/Pure/General/table.ML	Sat Feb 06 16:32:34 2010 +0100
@@ -28,7 +28,7 @@
   val keys: 'a table -> key list
   val min_key: 'a table -> key option
   val max_key: 'a table -> key option
-  val get_first: key option -> (key * 'a -> 'b option) -> 'a table -> 'b option
+  val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
   val exists: (key * 'a -> bool) -> 'a table -> bool
   val forall: (key * 'a -> bool) -> 'a table -> bool
   val lookup: 'a table -> key -> 'a option
@@ -131,40 +131,32 @@
 
 (* get_first *)
 
-fun get_first boundary f tab =
+fun get_first f =
   let
-    val check =
-      (case boundary of
-        NONE => K true
-      | SOME b => (fn k => Key.ord (b, k) = LESS));
-    fun apply (k, x) = if check k then f (k, x) else NONE;
-    fun get_bounded tb k = if check k then get tb else NONE
-    and get Empty = NONE
+    fun get Empty = NONE
       | get (Branch2 (left, (k, x), right)) =
-          (case get_bounded left k of
+          (case get left of
             NONE =>
-              (case apply (k, x) of
+              (case f (k, x) of
                 NONE => get right
               | some => some)
           | some => some)
       | get (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
-          (case get_bounded left k1 of
+          (case get left of
             NONE =>
-              (case apply (k1, x1) of
+              (case f (k1, x1) of
                 NONE =>
-                  (case get_bounded mid k2 of
+                  (case get mid of
                     NONE =>
-                      (case apply (k2, x2) of
+                      (case f (k2, x2) of
                         NONE => get right
                       | some => some)
                   | some => some)
               | some => some)
           | some => some);
-  in get tab end;
+  in get end;
 
-fun exists pred =
-  is_some o get_first NONE (fn entry => if pred entry then SOME () else NONE);
-
+fun exists pred = is_some o get_first (fn entry => if pred entry then SOME () else NONE);
 fun forall pred = not o exists (not o pred);