src/Doc/Isar_Ref/Inner_Syntax.thy

 subsection \<open>Abstract syntax trees \label{sec:ast}\<close>
 
 text \<open>The ML datatype @{ML_type Ast.ast} explicitly represents the
   intermediate AST format that is used for syntax rewriting
   (\secref{sec:syn-trans}).  It is defined in ML as follows:
-  \begin{ttbox}
-  datatype ast =
-    Constant of string |
-    Variable of string |
-    Appl of ast list
-  \end{ttbox}
+  @{verbatim [display]
+\<open>datatype ast =
+  Constant of string |
+  Variable of string |
+  Appl of ast list\<close>}
 
   An AST is either an atom (constant or variable) or a list of (at
   least two) subtrees.  Occasional diagnostic output of ASTs uses
   notation that resembles S-expression of LISP.  Constant atoms are
   shown as quoted strings, variable atoms as non-quoted strings and