src/HOL/Library/Fundamental_Theorem_Algebra.thy

--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Feb 18 22:46:47 2015 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Feb 18 22:46:48 2015 +0100
@@ -217,7 +217,7 @@
       using b v
       apply (simp add: th2)
       done
-    from mult_less_imp_less_left[OF th4 th3]
+    from mult_left_less_imp_less[OF th4 th3]
     have "?P ?w n" unfolding th1 .
     then have "\<exists>z. ?P z n" ..
   }