diff -r 2a0e1bcf713c -r 92f981f4a61b doc-src/Codegen/Thy/Refinement.thy
--- a/doc-src/Codegen/Thy/Refinement.thy	Sat Feb 18 20:06:43 2012 +0100
+++ b/doc-src/Codegen/Thy/Refinement.thy	Sat Feb 18 20:06:59 2012 +0100
@@ -265,12 +265,10 @@
 
 text {*
   Typical data structures implemented by representations involving
-  invariants are available in the library, e.g.~theories @{theory
-  Cset} and @{theory Mapping} specify sets (type @{typ "'a Cset.set"}) and
-  key-value-mappings (type @{typ "('a, 'b) mapping"}) respectively;
-  these can be implemented by distinct lists as presented here as
-  example (theory @{theory Dlist}) and red-black-trees respectively
-  (theory @{theory RBT}).
+  invariants are available in the library, theory @{theory Mapping}
+  specifies key-value-mappings (type @{typ "('a, 'b) mapping"});
+  these can be implemented by red-black-trees (theory @{theory RBT}).
 *}
 
 end
+