--- a/src/HOL/Real/Real.ML	Mon Aug 23 15:27:27 1999 +0200
+++ b/src/HOL/Real/Real.ML	Mon Aug 23 15:30:26 1999 +0200
@@ -715,7 +715,7 @@
 by (asm_full_simp_tac (simpset() addsimps 
 		       [real_rinv_distrib,real_add_mult_distrib,
 			real_mult_assoc RS sym]) 1);
-by (rtac (real_mult_assoc RS ssubst) 1);
+by (stac real_mult_assoc 1);
 by (rtac (real_mult_left_commute RS subst) 1);
 by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
 qed "real_rinv_add";