# HG changeset patch
# User haftmann
# Date 1497956869 -7200
# Node ID 4bf16fb7c14d84cb9c54d30a9e288b839beb1967
# Parent  5e60c2d0a1f156a0d0f006084f1278f7d55f60fe
deleting a code equation never leads to unimplemented function

diff -r 5e60c2d0a1f1 -r 4bf16fb7c14d NEWS
--- a/NEWS	Tue Jun 20 13:07:47 2017 +0200
+++ b/NEWS	Tue Jun 20 13:07:49 2017 +0200
@@ -74,6 +74,14 @@
 * Update to jedit-5.4.0.
 
 
+*** Pure ***
+
+* Deleting the last code equations for a particular function using
+[code del] results in function with no equations (runtime abort) rather
+than an unimplemented function (generate time abort).  Use explicit
+[[code drop:]] to enforce the latter.  Minor INCOMPATIBILTIY.
+
+
 *** HOL ***
 
 * "sublist" from theory List renamed to "nths" in analogy with "nth".
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;