deleting a code equation never leads to unimplemented function
authorhaftmann
Tue Jun 20 13:07:49 2017 +0200 (23 months ago)
changeset 661494bf16fb7c14d
parent 66148 5e60c2d0a1f1
child 66150 c2e19b9e1398
deleting a code equation never leads to unimplemented function
NEWS
src/Pure/Isar/code.ML
     1.1 --- a/NEWS	Tue Jun 20 13:07:47 2017 +0200
     1.2 +++ b/NEWS	Tue Jun 20 13:07:49 2017 +0200
     1.3 @@ -74,6 +74,14 @@
     1.4  * Update to jedit-5.4.0.
     1.5  
     1.6  
     1.7 +*** Pure ***
     1.8 +
     1.9 +* Deleting the last code equations for a particular function using
    1.10 +[code del] results in function with no equations (runtime abort) rather
    1.11 +than an unimplemented function (generate time abort).  Use explicit
    1.12 +[[code drop:]] to enforce the latter.  Minor INCOMPATIBILTIY.
    1.13 +
    1.14 +
    1.15  *** HOL ***
    1.16  
    1.17  * "sublist" from theory List renamed to "nths" in analogy with "nth".
     2.1 --- a/src/Pure/Isar/code.ML	Tue Jun 20 13:07:47 2017 +0200
     2.2 +++ b/src/Pure/Isar/code.ML	Tue Jun 20 13:07:49 2017 +0200
     2.3 @@ -1188,9 +1188,7 @@
     2.4        let
     2.5          fun del_eqn' (Eqns_Default _) = default_fun_spec
     2.6            | del_eqn' (Eqns eqns) =
     2.7 -              let
     2.8 -                val eqns' = filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns
     2.9 -              in if null eqns' then Unimplemented else Eqns eqns' end
    2.10 +              Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns)
    2.11            | del_eqn' spec = spec
    2.12        in change_fun_spec (const_eqn thy thm) del_eqn' thy end
    2.13    | NONE => thy;