| changeset 59582 | 0fbed69ff081 |
| parent 58878 | f962e42e324d |
| child 59867 | 58043346ca64 |
--- a/src/HOL/NSA/HyperDef.thy Tue Mar 03 19:08:04 2015 +0100 +++ b/src/HOL/NSA/HyperDef.thy Wed Mar 04 19:53:18 2015 +0100 @@ -338,7 +338,7 @@ *} simproc_setup fast_arith_hypreal ("(m::hypreal) < n" | "(m::hypreal) <= n" | "(m::hypreal) = 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 {* Exponentials on the Hyperreals *}