diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -95,30 +95,30 @@
   unfolding uminus_vec_def by simp
 
 instance vec :: (semigroup_add, finite) semigroup_add
-  by default (simp add: vec_eq_iff add.assoc)
+  by standard (simp add: vec_eq_iff add.assoc)
 
 instance vec :: (ab_semigroup_add, finite) ab_semigroup_add
-  by default (simp add: vec_eq_iff add.commute)
+  by standard (simp add: vec_eq_iff add.commute)
 
 instance vec :: (monoid_add, finite) monoid_add
-  by default (simp_all add: vec_eq_iff)
+  by standard (simp_all add: vec_eq_iff)
 
 instance vec :: (comm_monoid_add, finite) comm_monoid_add
-  by default (simp add: vec_eq_iff)
+  by standard (simp add: vec_eq_iff)
 
 instance vec :: (cancel_semigroup_add, finite) cancel_semigroup_add
-  by default (simp_all add: vec_eq_iff)
+  by standard (simp_all add: vec_eq_iff)
 
 instance vec :: (cancel_ab_semigroup_add, finite) cancel_ab_semigroup_add
-  by default (simp_all add: vec_eq_iff diff_diff_eq)
+  by standard (simp_all add: vec_eq_iff diff_diff_eq)
 
 instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add ..
 
 instance vec :: (group_add, finite) group_add
-  by default (simp_all add: vec_eq_iff)
+  by standard (simp_all add: vec_eq_iff)
 
 instance vec :: (ab_group_add, finite) ab_group_add
-  by default (simp_all add: vec_eq_iff)
+  by standard (simp_all add: vec_eq_iff)
 
 
 subsection \<open>Real vector space\<close>
@@ -132,7 +132,7 @@
   unfolding scaleR_vec_def by simp
 
 instance
-  by default (simp_all add: vec_eq_iff scaleR_left_distrib scaleR_right_distrib)
+  by standard (simp_all add: vec_eq_iff scaleR_left_distrib scaleR_right_distrib)
 
 end
 
@@ -412,7 +412,7 @@
 by (rule member_le_setL2) simp_all
 
 lemma bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
-apply default
+apply standard
 apply (rule vector_add_component)
 apply (rule vector_scaleR_component)
 apply (rule_tac x="1" in exI, simp add: norm_nth_le)