--- a/src/HOL/NSA/hypreal_arith.ML Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/NSA/hypreal_arith.ML Mon Mar 23 19:01:15 2009 +0100
@@ -30,10 +30,10 @@
Simplifier.simproc (the_context ())
"fast_hypreal_arith"
["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
- (K LinArith.lin_arith_simproc);
+ (K Lin_Arith.lin_arith_simproc);
val hypreal_arith_setup =
- LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+ Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms,
mult_mono_thms = mult_mono_thms,
inj_thms = real_inj_thms @ inj_thms,