--- a/src/HOL/Analysis/normarith.ML Wed Jan 31 21:05:47 2018 +0100
+++ b/src/HOL/Analysis/normarith.ML Thu Feb 01 13:55:10 2018 +0100
@@ -375,7 +375,7 @@
local
val rawrule = fconv_rule (arg_conv (rewr_conv @{thm real_eq_0_iff_le_ge_0}))
fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
- 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;
(* FIXME: Lookup in the context every time!!! Fix this !!!*)
fun splitequation ctxt th acc =
let