src/HOL/Library/positivstellensatz.ML
changeset 52049 156e12d5cb92
parent 51717 9e7d1c139569
child 58628 fd3c96a8ca60
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Fri May 17 11:35:52 2013 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Fri May 17 13:46:18 2013 +0200
     1.3 @@ -44,9 +44,10 @@
     1.4          in if z w then Tab.delete k t else Tab.update (k,w) t end;
     1.5    in Tab.fold h a b end;
     1.6  
     1.7 -fun choose f = case Tab.min_key f of
     1.8 -    SOME k => (k, the (Tab.lookup f k))
     1.9 -  | NONE => error "FuncFun.choose : Completely empty function"
    1.10 +fun choose f =
    1.11 +  (case Tab.min f of
    1.12 +    SOME entry => entry
    1.13 +  | NONE => error "FuncFun.choose : Completely empty function")
    1.14  
    1.15  fun onefunc kv = update kv empty
    1.16