src/Doc/Codegen/Adaptation.thy

   typically contains the keywords of the target language.  It can be
   extended manually, thus avoiding accidental overwrites, using the
   @{command_def "code_reserved"} command:
 \<close>
 
-code_reserved %quote "\<SMLdummy>" bool true false andalso
+code_reserved %quotett ("\<SMLdummy>") bool true false andalso
 
 text \<open>
   \noindent Next, we try to map HOL pairs to SML pairs, using the
   infix ``\<^verbatim>\<open>*\<close>'' type constructor and parentheses:
 \<close>

 code_printing %quotett code_module "Errno" \<rightharpoonup> (Haskell)
  \<open>module Errno(errno) where
 
   errno i = error ("Error number: " ++ show i)\<close>
 
-code_reserved %quotett Haskell Errno
+code_reserved %quotett (Haskell) Errno
 
 text \<open>
   \noindent Such named modules are then prepended to every
   generated code.  Inspect such code in order to find out how
   this behaves with respect to a particular