diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Hyperreal/hypreal_arith.ML
--- a/src/HOL/Hyperreal/hypreal_arith.ML	Mon Dec 29 06:49:26 2003 +0100
+++ b/src/HOL/Hyperreal/hypreal_arith.ML	Thu Jan 01 10:06:32 2004 +0100
@@ -214,8 +214,8 @@
 val hypreal_mult_mono_thms =
  [(rotate_prems 1 hypreal_mult_less_mono2,
    cvar(hypreal_mult_less_mono2, hd(prems_of hypreal_mult_less_mono2))),
-  (hypreal_mult_le_mono2,
-   cvar(hypreal_mult_le_mono2, hd(tl(prems_of hypreal_mult_le_mono2))))]
+  (mult_left_mono,
+   cvar(mult_left_mono, hd(tl(prems_of mult_left_mono))))]
 
 in