src/Doc/Codegen/Foundations.thy

   program, the code generator complains (since in most cases this is
   indeed an error).  But such constants can also be thought
   of as function definitions which always fail,
   since there is never a successful pattern match on the left hand
   side.  In order to categorise a constant into that category
-  explicitly, use @{command_def "code_abort"}:
-*}
-
-code_abort %quote empty_queue
+  explicitly, use the @{attribute code} attribute with
+  @{text abort}:
+*}
+
+declare %quote [[code abort: empty_queue]]
 
 text {*
   \noindent Then the code generator will just insert an error or
   exception at the appropriate position:
 *}

   @{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}
 *}
 
 text {*
   \noindent This feature however is rarely needed in practice.  Note
-  also that the HOL default setup already declares @{const undefined}
-  as @{command "code_abort"}, which is most likely to be used in such
-  situations.
+  also that the HOL default setup already declares @{const undefined},
+  which is most likely to be used in such situations, as
+  @{text "code abort"}.
 *}
 
 
 subsection {* If something goes utterly wrong \label{sec:utterly_wrong} *}