src/HOL/Library/positivstellensatz.ML
changeset 36700 9b85b9d74b83
parent 35408 b48ab741683b
child 36721 bfd7f5c3bf69
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed May 05 16:53:21 2010 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu May 06 16:32:20 2010 +0200
     1.3 @@ -748,7 +748,7 @@
     1.4    fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS
     1.5    val {add,mul,neg,pow,sub,main} = 
     1.6       Normalizer.semiring_normalizers_ord_wrapper ctxt
     1.7 -      (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) 
     1.8 +      (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) 
     1.9       simple_cterm_ord
    1.10  in gen_real_arith ctxt
    1.11     (cterm_of_rat, field_comp_conv, field_comp_conv,field_comp_conv,