diff -r 2a64142500f6 -r 279facb4253a src/HOL/Real/RealBin.ML
--- a/src/HOL/Real/RealBin.ML	Mon Dec 31 14:13:07 2001 +0100
+++ b/src/HOL/Real/RealBin.ML	Wed Jan 02 16:06:31 2002 +0100
@@ -18,7 +18,8 @@
 qed "real_numeral_0_eq_0";
 
 Goalw [real_number_of_def] "Numeral1 = (1::real)";
-by (simp_tac (simpset() addsimps [real_of_int_one RS sym]) 1);
+by (stac (real_of_one RS sym) 1); 
+by (Simp_tac 1); 
 qed "real_numeral_1_eq_1";
 
 (** Addition **)