src/HOL/HOLCF/Discrete.thy

--- a/src/HOL/HOLCF/Discrete.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/Discrete.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -19,7 +19,7 @@
   "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
 
 instance
-by default (simp add: below_discr_def)
+  by standard (simp add: below_discr_def)
 
 end