src/HOL/Library/positivstellensatz.ML
changeset 36751 7f1da69cacb3
parent 36721 bfd7f5c3bf69
child 36753 5cf4e9128f22
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Fri May 07 10:00:24 2010 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Fri May 07 15:05:52 2010 +0200
     1.3 @@ -751,7 +751,7 @@
     1.4        (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) 
     1.5       simple_cterm_ord
     1.6  in gen_real_arith ctxt
     1.7 -   (cterm_of_rat, Normalizer.field_comp_conv, Normalizer.field_comp_conv, Normalizer.field_comp_conv,
     1.8 +   (cterm_of_rat, Numeral_Simprocs.field_comp_conv, Numeral_Simprocs.field_comp_conv, Numeral_Simprocs.field_comp_conv,
     1.9      main,neg,add,mul, prover)
    1.10  end;
    1.11