--- 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".
--- 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;