src/HOL/Library/positivstellensatz.ML
changeset 36753 5cf4e9128f22
parent 36751 7f1da69cacb3
child 36945 9bec62c10714
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Fri May 07 16:12:25 2010 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Fri May 07 16:12:26 2010 +0200
     1.3 @@ -747,8 +747,8 @@
     1.4   let
     1.5    fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS
     1.6    val {add,mul,neg,pow,sub,main} = 
     1.7 -     Normalizer.semiring_normalizers_ord_wrapper ctxt
     1.8 -      (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) 
     1.9 +     Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
    1.10 +      (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) 
    1.11       simple_cterm_ord
    1.12  in gen_real_arith ctxt
    1.13     (cterm_of_rat, Numeral_Simprocs.field_comp_conv, Numeral_Simprocs.field_comp_conv, Numeral_Simprocs.field_comp_conv,