src/HOL/ex/Dedekind_Real.thy

--- a/src/HOL/ex/Dedekind_Real.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -1567,7 +1567,7 @@
   "(sup :: real \<Rightarrow> real \<Rightarrow> real) = max"
 
 instance
-  by default (auto simp add: inf_real_def sup_real_def max_min_distrib2)
+  by standard (auto simp add: inf_real_def sup_real_def max_min_distrib2)
 
 end