doc-src/Codegen/Thy/Evaluation.thy

   whole @{text SML} is read, the necessary code is generated transparently
   and the corresponding constant names are inserted.  This technique also
   allows to use pattern matching on constructors stemming from compiled
   @{text "datatypes"}.
 
-  For a less simplistic example, theory @{theory Ferrack} is
+  For a less simplistic example, theory @{text Ferrack} is
   a good reference.
 *}
 
 
 end