diff -r c40c9b05952c -r 1f1f9cbd23ae doc-src/Codegen/Thy/Further.thy
--- a/doc-src/Codegen/Thy/Further.thy	Mon May 31 10:29:04 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy	Mon May 31 17:29:26 2010 +0200
@@ -94,7 +94,7 @@
   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}.
+  @{text "datatypes"}.
 
   For a less simplistic example, theory @{theory Ferrack} is
   a good reference.