--- 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