--- a/src/HOL/Tools/semiring_normalizer.ML Wed Jan 31 21:05:47 2018 +0100
+++ b/src/HOL/Tools/semiring_normalizer.ML Thu Feb 01 13:55:10 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 = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS;
+fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS;
(* various normalizing conversions *)