diff -r c2524d123528 -r 7e6ffd8f51a9 src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Mon Apr 27 08:22:37 2009 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Mon Apr 27 10:11:44 2009 +0200
@@ -345,11 +345,10 @@
     by (simp add: up_inverse_def)
   show "p / q = p * inverse q"
     by (simp add: up_divide_def)
-  show "p * 1 = p"
-    unfolding `p * 1 = 1 * p` by (fact `1 * p = p`)
 qed
 
-instance up :: (ring) recpower ..
+instance up :: (ring) recpower proof
+qed simp_all
 
 (* Further properties of monom *)