src/HOL/Library/positivstellensatz.ML
changeset 33035 15eab423e573
parent 33002 f3f02f36a3e2
child 33039 5018f6a76b3f
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Tue Oct 20 23:25:04 2009 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Oct 21 00:36:12 2009 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4    in Tab.fold h a b end;
     1.5  
     1.6  fun choose f = case Tab.min_key f of 
     1.7 -   SOME k => (k,valOf (Tab.lookup f k))
     1.8 +   SOME k => (k, the (Tab.lookup f k))
     1.9   | NONE => error "FuncFun.choose : Completely empty function"
    1.10  
    1.11  fun onefunc kv = update kv empty
    1.12 @@ -743,7 +743,7 @@
    1.13    fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS
    1.14    val {add,mul,neg,pow,sub,main} = 
    1.15       Normalizer.semiring_normalizers_ord_wrapper ctxt
    1.16 -      (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) 
    1.17 +      (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) 
    1.18       simple_cterm_ord
    1.19  in gen_real_arith ctxt
    1.20     (cterm_of_rat, field_comp_conv, field_comp_conv,field_comp_conv,