# HG changeset patch
# User wenzelm
# Date 1517429147 -3600
#      Wed Jan 31 21:05:47 2018 +0100
# Node ID eb37b77e9a685dc603855744ee7a59e4a4ac6624
# Parent  64b47495676d5d6bdec02032a7a90fe6e1ff6c50
proper term_ord as in HOL/Library/positivstellensatz.ML, e.g. relevant for "0 <= c & 0 <= a ==> a + bb = 1 & c <= 1 ==> bb * c * 4 <= (12::real)";

diff -r 64b47495676d -r eb37b77e9a68 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Oct 04 12:00:53 2017 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Jan 31 21:05:47 2018 +0100
@@ -750,7 +750,7 @@
 local
   open Conv
   val concl = Thm.dest_arg o Thm.cprop_of
-  fun simple_cterm_ord t u = Term_Ord.fast_term_ord (Thm.term_of t, Thm.term_of u) = LESS
+  fun simple_cterm_ord t u = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS
 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 = Term_Ord.fast_term_ord (Thm.term_of t, Thm.term_of u) = LESS
+  fun simple_cterm_ord t u = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS
   val concl = Thm.dest_arg o Thm.cprop_of
   val shuffle1 =
     fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))"