diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/Library/Univ_Poly.thy
--- a/src/HOL/Library/Univ_Poly.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Library/Univ_Poly.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -204,7 +204,7 @@
     from Cons.hyps[rule_format, of x]
     obtain q r where qr: "x#xs = [r] +++ [- a, 1] *** q" by blast
     have "h#x#xs = [a*r + h] +++ [-a, 1] *** (r#q)"
-      using qr by(cases q, simp_all add: algebra_simps diff_def[symmetric]
+      using qr by(cases q, simp_all add: algebra_simps diff_minus[symmetric]
         minus_mult_left[symmetric] right_minus)
     hence "\<exists>q r. h#x#xs = [r] +++ [-a, 1] *** q" by blast}
   thus ?case by blast