src/HOL/Library/positivstellensatz.ML
changeset 67560 0fa87bd86566
parent 67559 833d154ab189
child 67562 2427d3e72b6e
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Thu Feb 01 13:55:10 2018 +0100
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu Feb 01 15:12:57 2018 +0100
     1.3 @@ -764,7 +764,7 @@
     1.4  
     1.5  fun gen_prover_real_arith ctxt prover =
     1.6    let
     1.7 -    fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS
     1.8 +    fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u))
     1.9      val {add, mul, neg, pow = _, sub = _, main} =
    1.10          Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
    1.11          (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>))