src/HOL/Library/positivstellensatz.ML
changeset 36721 bfd7f5c3bf69
parent 36700 9b85b9d74b83
child 36751 7f1da69cacb3
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Thu May 06 23:11:57 2010 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu May 06 23:11:57 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, field_comp_conv, field_comp_conv,field_comp_conv,
     1.8 +   (cterm_of_rat, Normalizer.field_comp_conv, Normalizer.field_comp_conv, Normalizer.field_comp_conv,
     1.9      main,neg,add,mul, prover)
    1.10  end;
    1.11