--- 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
--- 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;
--- 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
--- 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))
--- 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)
--- 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 *)
--- 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, ...}) =