Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned min_key, max_key;
authorwenzelm
Fri, 15 Jul 2005 15:44:19 +0200
changeset 16864 0f536ece46e3
parent 16863 79b9a6481ae4
child 16865 fb39dcfc1c24
tuned min_key, max_key;
src/Pure/General/table.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/General/table.ML	Fri Jul 15 15:44:18 2005 +0200
+++ b/src/Pure/General/table.ML	Fri Jul 15 15:44:19 2005 +0200
@@ -115,12 +115,16 @@
 end;
 
 fun min_key Empty = NONE
-  | min_key (Branch2 (left, (k, _), _)) = SOME (if_none (min_key left) k)
-  | min_key (Branch3 (left, (k, _), _, _, _)) = SOME (if_none (min_key left) k);
+  | 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 max_key Empty = NONE
-  | max_key (Branch2 (_, (k, _), right)) = SOME (if_none (max_key right) k)
-  | max_key (Branch3 (_, _, _, (k,_), right)) = SOME (if_none (max_key right) k);
+  | 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;
 
 
 (* lookup *)
isabelle