diff -r cbc38731d42f -r 0fbed69ff081 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Nat.thy	Wed Mar 04 19:53:18 2015 +0100
@@ -1629,7 +1629,7 @@
 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