src/HOL/Int.thy

 declaration {* K Int_Arith.setup *}
 
 simproc_setup fast_arith ("(m::'a::linordered_idom) < n" |
   "(m::'a::linordered_idom) <= n" |
   "(m::'a::linordered_idom) = n") =
-  {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
+  {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (Thm.term_of ct) *}
 
 
 subsection{*More Inequality Reasoning*}
 
 lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"