# HG changeset patch
# User wenzelm
# Date 1517429147 -3600
# Node ID c46910a6bfce9419c0573ea09217d9bc2c301acf
# Parent  a965ccf7414e2f4deef60dbe75dcd32a959b5e61
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 a965ccf7414e -r c46910a6bfce src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Jan 31 14:20:39 2018 +0100
+++ 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))"