diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -141,22 +141,22 @@
   done
 
 lemmas scaleR_right_has_derivative =
-  bounded_linear.has_derivative [OF bounded_linear_scaleR_right, standard]
+  bounded_linear.has_derivative [OF bounded_linear_scaleR_right]
 
 lemmas scaleR_left_has_derivative =
-  bounded_linear.has_derivative [OF bounded_linear_scaleR_left, standard]
+  bounded_linear.has_derivative [OF bounded_linear_scaleR_left]
 
 lemmas inner_right_has_derivative =
-  bounded_linear.has_derivative [OF bounded_linear_inner_right, standard]
+  bounded_linear.has_derivative [OF bounded_linear_inner_right]
 
 lemmas inner_left_has_derivative =
-  bounded_linear.has_derivative [OF bounded_linear_inner_left, standard]
+  bounded_linear.has_derivative [OF bounded_linear_inner_left]
 
 lemmas mult_right_has_derivative =
-  bounded_linear.has_derivative [OF bounded_linear_mult_right, standard]
+  bounded_linear.has_derivative [OF bounded_linear_mult_right]
 
 lemmas mult_left_has_derivative =
-  bounded_linear.has_derivative [OF bounded_linear_mult_left, standard]
+  bounded_linear.has_derivative [OF bounded_linear_mult_left]
 
 lemmas euclidean_component_has_derivative =
   bounded_linear.has_derivative [OF bounded_linear_euclidean_component]