src/HOL/Int.thy
changeset 59582 0fbed69ff081
parent 59556 aa2deef7cf47
child 59613 7103019278f0
     1.1 --- a/src/HOL/Int.thy	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/Int.thy	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -753,7 +753,7 @@
     1.4  simproc_setup fast_arith ("(m::'a::linordered_idom) < n" |
     1.5    "(m::'a::linordered_idom) <= n" |
     1.6    "(m::'a::linordered_idom) = n") =
     1.7 -  {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
     1.8 +  {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (Thm.term_of ct) *}
     1.9  
    1.10  
    1.11  subsection{*More Inequality Reasoning*}