1.1 --- a/src/HOL/ex/Numeral.thy	Thu Aug 28 22:08:02 2008 +0200
     1.2 +++ b/src/HOL/ex/Numeral.thy	Thu Aug 28 22:08:11 2008 +0200
     1.3 @@ -397,7 +397,7 @@
     1.4  lemma of_num_plus [numeral]:
     1.5    "of_num m + of_num n = of_num (m + n)"
     1.6    by (induct n rule: num_induct)
     1.7 -    (simp_all add: Dig_plus of_num_one semigroup_add_class.plus.add_assoc [symmetric, of m]
     1.8 +    (simp_all add: Dig_plus of_num_one semigroup_add_class.add_assoc [symmetric, of m]
     1.9      add_ac of_num_plus_one [symmetric])
    1.10  
    1.11  lemma of_num_times_one [numeral]:
    1.12 @@ -412,7 +412,7 @@
    1.13    "of_num m * of_num n = of_num (m * n)"
    1.14    by (induct n rule: num_induct)
    1.15      (simp_all add: of_num_plus [symmetric]
    1.16 -    semiring_class.plus_times.right_distrib right_distrib of_num_one)
    1.17 +    semiring_class.right_distrib right_distrib of_num_one)
    1.18  
    1.19  end
    1.20