--- 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