[isabelle-dev] Should code_abort remove the corresponding code equations?

[Johannes Hölzl]

Hi *,

code_abort does not remove the corresponding code equations
(in Isabelle 19764bef2730)

  definition "test = True"
  code_abort test
  value [code] test -- "outputs True"

  definition [code del]: "test2 = True"
  code_abort test2
  value [code] test2 -- "raises 'test' exception"

Should code_abort remove the code equation for test? Otherwise the
resulting program might be non-terminating.

Greetings,
 - Johannes