diff -r d995733b635d -r f0de18b62d63 src/HOL/Import/HOLLightReal.thy
--- a/src/HOL/Import/HOLLightReal.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Import/HOLLightReal.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -112,7 +112,7 @@
 
 lemma REAL_DIFFSQ:
   "((x :: real) + y) * (x - y) = x * x - y * y"
-  by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) mult.add_right mult_diff_mult)
+  by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) right_distrib mult_diff_mult)
 
 lemma REAL_ABS_TRIANGLE_LE:
   "abs (x :: real) + abs (y - x) \<le> z \<longrightarrow> abs y \<le> z"
@@ -295,7 +295,7 @@
    (\<forall>(x :: real). 0 * x = 0) \<and>
    (\<forall>(x :: real) y z. x * (y + z) = x * y + x * z) \<and>
    (\<forall>(x :: real). x ^ 0 = 1) \<and> (\<forall>(x :: real) n. x ^ Suc n = x * x ^ n)"
-  by (auto simp add: mult.add_right)
+  by (auto simp add: right_distrib)
 
 lemma REAL_COMPLETE:
   "(\<exists>(x :: real). P x) \<and> (\<exists>(M :: real). \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>