--- 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,