diff -r d3d2b78b1c19 -r a8cc904a6820 src/HOL/Library/ListVector.thy
--- a/src/HOL/Library/ListVector.thy	Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Library/ListVector.thy	Fri Oct 19 15:12:52 2012 +0200
@@ -128,7 +128,7 @@
 apply simp
 apply(case_tac zs)
 apply (simp)
-apply(simp add: left_distrib)
+apply(simp add: distrib_right)
 done
 
 lemma iprod_left_diff_distrib: "\<langle>xs - ys, zs\<rangle> = \<langle>xs,zs\<rangle> - \<langle>ys,zs\<rangle>"
@@ -146,7 +146,7 @@
 apply simp
 apply(case_tac ys)
 apply (simp)
-apply (simp add: right_distrib mult_assoc)
+apply (simp add: distrib_left mult_assoc)
 done
 
 end