doc-src/IsarAdvanced/Codegen/Thy/ML.thy

   Implementing code generator applications on top
   of the framework set out so far usually not only
   involves using those primitive interfaces
   but also storing code-dependent data and various
   other things.
-
-  \begin{warn}
-    Some interfaces discussed here have not reached
-    a final state yet.
-    Changes likely to occur in future.
-  \end{warn}
 *}
 
 subsubsection {* Data depending on the theory's executable content *}
 
 text {*

     hints that executable content for constants @{text consts}
     has changed.
 
   \end{description}
 
-  An instance of @{ML_functor CodeDataFun} provides the following
+  \noindent An instance of @{ML_functor CodeDataFun} provides the following
   interface:
 
   \medskip
   \begin{tabular}{l}
   @{text "get: theory \<rightarrow> T"} \\

 
   \end{description}
 *}
 
 text {*
+  \bigskip
+
   \emph{Happy proving, happy hacking!}
 *}
 
 end