diff -r 8e562d56d404 -r 0b8a5fd339ab src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sat Mar 06 16:02:22 2010 -0800
+++ b/src/HOL/Parity.thy	Sat Mar 06 18:24:30 2010 -0800
@@ -218,7 +218,7 @@
   done
 
 lemma zero_le_even_power: "even n ==>
-    0 <= (x::'a::{linordered_ring_strict,monoid_mult}) ^ n"
+    0 <= (x::'a::{linordered_ring,monoid_mult}) ^ n"
   apply (simp add: even_nat_equiv_def2)
   apply (erule exE)
   apply (erule ssubst)