--- a/src/HOL/Tools/semiring_normalizer.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/HOL/Tools/semiring_normalizer.ML Thu Feb 01 15:12:57 2018 +0100
@@ -851,7 +851,7 @@
addsimps (@{thms eval_nat_numeral} @ @{thms diff_nat_numeral} @ @{thms arith_simps} @ @{thms rel_simps})
addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}]);
-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));
(* various normalizing conversions *)