--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Thu Feb 01 15:12:57 2018 +0100
@@ -750,7 +750,7 @@
local
open Conv
val concl = Thm.dest_arg o Thm.cprop_of
- fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS
+ fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u))
in
(* FIXME: Replace tryfind by get_first !! *)
fun real_nonlinear_prover proof_method ctxt =
@@ -851,7 +851,7 @@
local
open Conv
- fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS
+ fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u))
val concl = Thm.dest_arg o Thm.cprop_of
val shuffle1 =
fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))"