diff -r fe12dc60bc3c -r e3229a37d53f src/HOL/Real/RComplete.ML
--- a/src/HOL/Real/RComplete.ML	Wed Dec 06 12:28:52 2000 +0100
+++ b/src/HOL/Real/RComplete.ML	Wed Dec 06 12:34:12 2000 +0100
@@ -202,8 +202,8 @@
         Related: Archimedean property of reals
  ----------------------------------------------------------------*)
 
-Goal "#0 < x ==> EX n. rinv(real_of_posnat n) < x";
-by (stac real_of_posnat_rinv_Ex_iff 1);
+Goal "#0 < x ==> EX n. inverse (real_of_posnat n) < x";
+by (stac real_of_posnat_inverse_Ex_iff 1);
 by (EVERY1[rtac ccontr, Asm_full_simp_tac]);
 by (fold_tac [real_le_def]);
 by (subgoal_tac "isUb (UNIV::real set) \
@@ -233,9 +233,9 @@
 by (res_inst_tac [("x","0")] exI 2);
 by (auto_tac (claset() addEs [real_less_trans],
 	      simpset() addsimps [real_of_posnat_one,real_zero_less_one]));
-by (ftac ((rename_numerals real_rinv_gt_zero) RS reals_Archimedean) 1);
+by (ftac ((rename_numerals real_inverse_gt_zero) RS reals_Archimedean) 1);
 by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
-by (forw_inst_tac [("y","rinv x")]
+by (forw_inst_tac [("y","inverse x")]
     (rename_numerals real_mult_less_mono1) 1);
 by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym]));
 by (dres_inst_tac [("n1","n"),("y","#1")]