src/HOL/Int.thy

--- a/src/HOL/Int.thy	Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Int.thy	Wed Mar 04 19:53:18 2015 +0100
@@ -753,7 +753,7 @@
 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*}