diff -r 5e60c2d0a1f1 -r 4bf16fb7c14d src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Jun 20 13:07:47 2017 +0200
+++ b/src/Pure/Isar/code.ML	Tue Jun 20 13:07:49 2017 +0200
@@ -1188,9 +1188,7 @@
       let
         fun del_eqn' (Eqns_Default _) = default_fun_spec
           | del_eqn' (Eqns eqns) =
-              let
-                val eqns' = filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns
-              in if null eqns' then Unimplemented else Eqns eqns' end
+              Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns)
           | del_eqn' spec = spec
       in change_fun_spec (const_eqn thy thm) del_eqn' thy end
   | NONE => thy;