diff -r cc0b4bbfbc43 -r f17ca9f6dc8c src/HOL/Real/RComplete.ML
--- a/src/HOL/Real/RComplete.ML	Fri Dec 19 10:38:48 2003 +0100
+++ b/src/HOL/Real/RComplete.ML	Fri Dec 19 17:13:28 2003 +0100
@@ -199,7 +199,7 @@
 by (rtac ccontr 1);
 by (subgoal_tac "ALL n. x * real (Suc n) <= 1" 1);
 by (asm_full_simp_tac
-    (simpset() addsimps [linorder_not_less, real_inverse_eq_divide]) 2); 
+    (simpset() addsimps [linorder_not_less, inverse_eq_divide]) 2); 
 by (Clarify_tac 2);
 by (dres_inst_tac [("x","n")] spec 2); 
 by (dres_inst_tac [("k","real (Suc n)")] (real_mult_le_mono1) 2);