1.1 --- a/src/HOL/Real/RealBin.ML	Mon Dec 31 14:13:07 2001 +0100
     1.2 +++ b/src/HOL/Real/RealBin.ML	Wed Jan 02 16:06:31 2002 +0100
     1.3 @@ -18,7 +18,8 @@
     1.4  qed "real_numeral_0_eq_0";
     1.5  
     1.6  Goalw [real_number_of_def] "Numeral1 = (1::real)";
     1.7 -by (simp_tac (simpset() addsimps [real_of_int_one RS sym]) 1);
     1.8 +by (stac (real_of_one RS sym) 1); 
     1.9 +by (Simp_tac 1); 
    1.10  qed "real_numeral_1_eq_1";
    1.11  
    1.12  (** Addition **)