src/HOL/Multivariate_Analysis/Euclidean_Space.thy

--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -139,7 +139,7 @@
   [simp]: "Basis = {1::real}"
 
 instance
-  by default auto
+  by standard auto
 
 end
 
@@ -155,7 +155,7 @@
   "Basis = {1, ii}"
 
 instance
-  by default (auto simp add: Basis_complex_def intro: complex_eqI split: split_if_asm)
+  by standard (auto simp add: Basis_complex_def intro: complex_eqI split: split_if_asm)
 
 end