diff -r 1dd7439477dd -r efda5615bb7d src/HOL/Real/real_arith.ML
--- a/src/HOL/Real/real_arith.ML	Mon Dec 22 14:12:54 2003 +0100
+++ b/src/HOL/Real/real_arith.ML	Mon Dec 22 15:41:25 2003 +0100
@@ -9,7 +9,8 @@
 
 (** Misc ML bindings **)
 
-val inverse_less_iff_less = thm"inverse_less_iff_less";
+val inverse_less_iff_less = thm"Ring_and_Field.inverse_less_iff_less";
+val add_right_mono = thm"Ring_and_Field.add_right_mono";
 
 val pos_real_less_divide_eq = thm"pos_less_divide_eq";
 val pos_real_divide_less_eq = thm"pos_divide_less_eq";