src/HOL/Nat.thy

 ML_file "Tools/lin_arith.ML"
 setup {* Lin_Arith.global_setup *}
 declaration {* K Lin_Arith.setup *}
 
 simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) <= n" | "(m::nat) = 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) *}
 (* Because of this simproc, the arithmetic solver is really only
 useful to detect inconsistencies among the premises for subgoals which are
 *not* themselves (in)equalities, because the latter activate
 fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
 solver all the time rather than add the additional check. *)