diff -r 16a2ed09217a -r 4517a4049588 doc-src/Codegen/Thy/Setup.thy
--- a/doc-src/Codegen/Thy/Setup.thy	Thu Sep 02 16:41:42 2010 +0200
+++ b/doc-src/Codegen/Thy/Setup.thy	Thu Sep 02 16:41:44 2010 +0200
@@ -1,15 +1,12 @@
 theory Setup
-imports Complex_Main More_List RBT Dlist Mapping
+imports
+  Complex_Main
+  More_List RBT Dlist Mapping
 uses
   "../../antiquote_setup.ML"
   "../../more_antiquote.ML"
 begin
 
-ML {* no_document use_thys
-  ["Efficient_Nat", "Code_Char_chr", "Product_ord",
-   "~~/src/HOL/Imperative_HOL/Imperative_HOL",
-   "~~/src/HOL/Decision_Procs/Ferrack"] *}
-
 setup {*
 let
   val typ = Simple_Syntax.read_typ;