diff -r 4044f53326c9 -r 05573e5504a9 src/HOL/Multivariate_Analysis/Fashoda.thy
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Wed Feb 18 22:46:47 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Wed Feb 18 22:46:48 2015 +0100
@@ -590,7 +590,7 @@
       then have "(1 - u) * b > (1 - u) * a"
         by (auto simp add:field_simps)
       then have "b \<ge> a"
-        apply (drule_tac mult_less_imp_less_left)
+        apply (drule_tac mult_left_less_imp_less)
         using u
         apply auto
         done
@@ -607,7 +607,7 @@
       then have "(1 - u) * a \<le> (1 - u) * b"
         apply -
         apply (rule mult_left_mono)
-        apply (drule mult_less_imp_less_left)
+        apply (drule mult_left_less_imp_less)
         using u
         apply auto
         done
@@ -671,7 +671,7 @@
       then have "(1 - u) * b > (1 - u) * a"
         by (auto simp add: field_simps)
       then have "b \<ge> a"
-        apply (drule_tac mult_less_imp_less_left)
+        apply (drule_tac mult_left_less_imp_less)
         using u
         apply auto
         done
@@ -688,7 +688,7 @@
       then have "(1 - u) * a \<le> (1 - u) * b"
         apply -
         apply (rule mult_left_mono)
-        apply (drule mult_less_imp_less_left)
+        apply (drule mult_left_less_imp_less)
         using u
         apply auto
         done