src/HOL/Library/positivstellensatz.ML
changeset 67562 2427d3e72b6e
parent 67560 0fa87bd86566
child 67564 d615e9ca77dc
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Thu Feb 01 15:31:25 2018 +0100
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu Feb 01 17:15:07 2018 +0100
     1.3 @@ -764,11 +764,10 @@
     1.4  
     1.5  fun gen_prover_real_arith ctxt prover =
     1.6    let
     1.7 -    fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u))
     1.8      val {add, mul, neg, pow = _, sub = _, main} =
     1.9          Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
    1.10          (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>))
    1.11 -        simple_cterm_ord
    1.12 +        Thm.term_ord
    1.13    in gen_real_arith ctxt
    1.14       (cterm_of_rat,
    1.15        Numeral_Simprocs.field_comp_conv ctxt,