src/Doc/Datatypes/Datatypes.thy

 
 @{rail "
   @@{command datatype_new} target? @{syntax dt_options}? \\
     (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
   ;
-  @{syntax_def dt_options}: '(' (('no_discs_sels' | 'rep_compat') + ',') ')'
+  @{syntax_def dt_options}: '(' (('no_discs_sels' | 'no_code' | 'rep_compat') + ',') ')'
 "}
 
 The syntactic entity \synt{target} can be used to specify a local
 context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference
 manual \cite{isabelle-isar-ref}.

 \setlength{\itemsep}{0pt}
 
 \item
 The @{text "no_discs_sels"} option indicates that no discriminators or selectors
 should be generated.
+
+\item
+The @{text "no_code"} option indicates that the datatype should not be
+registered for code generation.
 
 \item
 The @{text "rep_compat"} option indicates that the generated names should
 contain optional (and normally not displayed) ``@{text "new."}'' components to
 prevent clashes with a later call to \keyw{rep\_datatype}. See

 %
 %  * also useful for compatibility with old package, e.g. add destructors to
 %    old \keyw{datatype}
 %
 %  * @{command wrap_free_constructors}
-%    * @{text "no_discs_sels"}, @{text "rep_compat"}
+%    * @{text "no_discs_sels"}, @{text "no_code"}, @{text "rep_compat"}
 %    * hack to have both co and nonco view via locale (cf. ext nats)
 %  * code generator
 %     * eq, refl, simps
 *}
 

   @{syntax_def name_term}: (name ':' term)
   ;
   X_list: '[' (X + ',') ']'
 "}
 
-% options: no_discs_sels rep_compat
+% options: no_discs_sels no_code rep_compat
 
 \noindent
 Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.
 *}