src/HOL/Library/positivstellensatz.ML

--- a/src/HOL/Library/positivstellensatz.ML	Thu May 06 23:11:57 2010 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Thu May 06 23:11:57 2010 +0200
@@ -751,7 +751,7 @@
       (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) 
      simple_cterm_ord
 in gen_real_arith ctxt
-   (cterm_of_rat, field_comp_conv, field_comp_conv,field_comp_conv,
+   (cterm_of_rat, Normalizer.field_comp_conv, Normalizer.field_comp_conv, Normalizer.field_comp_conv,
     main,neg,add,mul, prover)
 end;