# HG changeset patch
# User wenzelm
# Date 1368791178 -7200
# Node ID 156e12d5cb92d574ff9349aea8183bc830d99dc9
# Parent  9003b293e775592d6dc2f9003d8eed184f1eefb2
tuned signature;

diff -r 9003b293e775 -r 156e12d5cb92 src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Fri May 17 11:35:52 2013 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Fri May 17 13:46:18 2013 +0200
@@ -44,9 +44,10 @@
         in if z w then Tab.delete k t else Tab.update (k,w) t end;
   in Tab.fold h a b end;
 
-fun choose f = case Tab.min_key f of
-    SOME k => (k, the (Tab.lookup f k))
-  | NONE => error "FuncFun.choose : Completely empty function"
+fun choose f =
+  (case Tab.min f of
+    SOME entry => entry
+  | NONE => error "FuncFun.choose : Completely empty function")
 
 fun onefunc kv = update kv empty
 
diff -r 9003b293e775 -r 156e12d5cb92 src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML
--- a/src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML	Fri May 17 11:35:52 2013 +0200
+++ b/src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML	Fri May 17 13:46:18 2013 +0200
@@ -263,11 +263,11 @@
 fun m_elem_at m i = Inttab.lookup m i
 
 fun v_only_elem v =
-    case Inttab.min_key v of
+    case Inttab.min v of
         NONE => NONE
-      | SOME vmin => (case Inttab.max_key v of
+      | SOME (vmin, _) => (case Inttab.max v of
                           NONE => SOME vmin
-                        | SOME vmax => if vmin = vmax then SOME vmin else NONE)
+                        | SOME (vmax, _) => if vmin = vmax then SOME vmin else NONE)
 
 fun v_fold f = Inttab.fold f;
 fun m_fold f = Inttab.fold f;
diff -r 9003b293e775 -r 156e12d5cb92 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Fri May 17 11:35:52 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Fri May 17 13:46:18 2013 +0200
@@ -42,7 +42,7 @@
   (let val v = hd (Inttab.lookup_list tab key) in
     (v, Inttab.remove_list (op =) (key, v) tab)
   end) handle List.Empty => raise Fail "sledgehammer_compress: pop"
-fun pop_max tab = pop tab (the (Inttab.max_key tab))
+fun pop_max tab = pop tab (fst (the (Inttab.max tab)))
   handle Option.Option => raise Fail "sledgehammer_compress: pop_max"
 fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab
 
diff -r 9003b293e775 -r 156e12d5cb92 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Fri May 17 11:35:52 2013 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Fri May 17 13:46:18 2013 +0200
@@ -365,7 +365,7 @@
             (* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
             val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm
             (* initialize the clause array with the given clauses *)
-            val max_idx = the (Inttab.max_key clause_table)
+            val max_idx = fst (the (Inttab.max clause_table))
             val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
             val _ =
               fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1))
diff -r 9003b293e775 -r 156e12d5cb92 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Fri May 17 11:35:52 2013 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Fri May 17 13:46:18 2013 +0200
@@ -856,8 +856,8 @@
               val _   = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".")
               (* set 'clause_offset' to the largest used clause ID *)
               val _   = if !clause_offset = ~1 then clause_offset :=
-                (case Inttab.max_key (!clause_table) of
-                  SOME id => id
+                (case Inttab.max (!clause_table) of
+                  SOME (id, _) => id
                 | NONE => cnf_number_of_clauses (Prop_Logic.defcnf fm) - 1  (* the first clause ID is 0, not 1 *))
                 else
                   ()
@@ -899,7 +899,7 @@
               (* for its literals to obtain the empty clause                *)
               val vids         = map (fn l => l div 2) ls
               val rs           = cid :: map (fn v => !clause_offset + v) vids
-              val new_empty_id = the_default (!clause_offset) (Inttab.max_key (!clause_table)) + 1
+              val new_empty_id = the_default (!clause_offset) (Option.map fst (Inttab.max (!clause_table))) + 1
             in
               (* update clause table and conflict id *)
               clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table)
diff -r 9003b293e775 -r 156e12d5cb92 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Fri May 17 11:35:52 2013 +0200
+++ b/src/Pure/General/table.ML	Fri May 17 13:46:18 2013 +0200
@@ -25,8 +25,8 @@
   val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
   val dest: 'a table -> (key * 'a) list
   val keys: 'a table -> key list
-  val min_key: 'a table -> key option
-  val max_key: 'a table -> key option
+  val min: 'a table -> (key * 'a) option
+  val max: 'a table -> (key * 'a) 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
@@ -116,19 +116,19 @@
 fun keys tab = fold_rev_table (cons o #1) tab [];
 
 
-(* min/max keys *)
+(* min/max entries *)
 
-fun min_key Empty = NONE
-  | min_key (Branch2 (Empty, (k, _), _)) = SOME k
-  | min_key (Branch3 (Empty, (k, _), _, _, _)) = SOME k
-  | min_key (Branch2 (left, _, _)) = min_key left
-  | min_key (Branch3 (left, _, _, _, _)) = min_key left;
+fun min Empty = NONE
+  | min (Branch2 (Empty, p, _)) = SOME p
+  | min (Branch3 (Empty, p, _, _, _)) = SOME p
+  | min (Branch2 (left, _, _)) = min left
+  | min (Branch3 (left, _, _, _, _)) = min left;
 
-fun max_key Empty = NONE
-  | max_key (Branch2 (_, (k, _), Empty)) = SOME k
-  | max_key (Branch3 (_, _, _, (k, _), Empty)) = SOME k
-  | max_key (Branch2 (_, _, right)) = max_key right
-  | max_key (Branch3 (_, _, _, _, right)) = max_key right;
+fun max Empty = NONE
+  | max (Branch2 (_, p, Empty)) = SOME p
+  | max (Branch3 (_, _, _, p, Empty)) = SOME p
+  | max (Branch2 (_, _, right)) = max right
+  | max (Branch3 (_, _, _, _, right)) = max right;
 
 
 (* get_first *)
diff -r 9003b293e775 -r 156e12d5cb92 src/Pure/envir.ML
--- a/src/Pure/envir.ML	Fri May 17 11:35:52 2013 +0200
+++ b/src/Pure/envir.ML	Fri May 17 13:46:18 2013 +0200
@@ -128,8 +128,8 @@
 
 (*Determine if the least index updated exceeds lim*)
 fun above (Envir {tenv, tyenv, ...}) lim =
-  (case Vartab.min_key tenv of SOME (_, i) => i > lim | NONE => true) andalso
-  (case Vartab.min_key tyenv of SOME (_, i) => i > lim | NONE => true);
+  (case Vartab.min tenv of SOME ((_, i), _) => i > lim | NONE => true) andalso
+  (case Vartab.min tyenv of SOME ((_, i), _) => i > lim | NONE => true);
 
 (*Update, checking Var-Var assignments: try to suppress higher indexes*)
 fun vupdate (aU as (a, U), t) (env as Envir {tyenv, ...}) =