diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/DAList.thy
--- a/src/HOL/Library/DAList.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/DAList.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -93,7 +93,7 @@
 definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys"
 
 instance
-  by default (simp add: equal_alist_def impl_of_inject)
+  by standard (simp add: equal_alist_def impl_of_inject)
 
 end