src/HOL/Library/DAList.thy
changeset 60679 ade12ef2773c
parent 59581 09722854b8f4
child 60919 b0ba7799d05a
--- 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