diff -r dcdfb6355a05 -r 4de9ff3ea29a 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 \ :: 'a discr \ 'a discr \ bool) = (op =)" instance -by default (simp add: below_discr_def) + by standard (simp add: below_discr_def) end