diff -r f0b11413f1c9 -r 2427d3e72b6e src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Thu Feb 01 15:31:25 2018 +0100
+++ b/src/HOL/Library/positivstellensatz.ML	Thu Feb 01 17:15:07 2018 +0100
@@ -764,11 +764,10 @@
 
 fun gen_prover_real_arith ctxt prover =
   let
-    fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u))
     val {add, mul, neg, pow = _, sub = _, main} =
         Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
         (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>))
-        simple_cterm_ord
+        Thm.term_ord
   in gen_real_arith ctxt
      (cterm_of_rat,
       Numeral_Simprocs.field_comp_conv ctxt,