doc-src/Codegen/Thy/Adaption.thy

 *}
 
 subsection {* The adaption principle *}
 
 text {*
-  The following figure illustrates what \qt{adaption} is conceptually
+  Figure \ref{fig:adaption} illustrates what \qt{adaption} is conceptually
   supposed to be:
 
   \begin{figure}[here]
     \includegraphics{Thy/pictures/adaption}
     \caption{The adaption principle}

 
 definition %quote "eq_class.eq (x\<Colon>bar) y \<longleftrightarrow> x = y"
 
 instance %quote by default (simp add: eq_bar_def)
 
-end %quote
-code_type %quotett bar
+end %quote (*<*)
+
+(*>*) code_type %quotett bar
   (Haskell "Integer")
 
 text {*
   \noindent The code generator would produce
   an additional instance, which of course is rejected by the @{text Haskell}