diff -r 10097e0a9dbd -r 2b4430847310 src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Fri Oct 01 16:05:25 2010 +0200
+++ b/src/Tools/Code_Generator.thy	Fri Oct 01 17:06:49 2010 +0200
@@ -2,7 +2,7 @@
     Author:  Florian Haftmann, TU Muenchen
 *)
 
-header {* Loading the code generator modules *}
+header {* Loading the code generator and related modules *}
 
 theory Code_Generator
 imports Pure
@@ -21,8 +21,8 @@
   "~~/src/Tools/Code/code_ml.ML"
   "~~/src/Tools/Code/code_haskell.ML"
   "~~/src/Tools/Code/code_scala.ML"
-  "~~/src/Tools/nbe.ML"
   ("~~/src/Tools/Code/code_runtime.ML")
+  ("~~/src/Tools/nbe.ML")
 begin
 
 setup {*
@@ -32,7 +32,6 @@
   #> Code_ML.setup
   #> Code_Haskell.setup
   #> Code_Scala.setup
-  #> Nbe.setup
   #> Quickcheck.setup
 *}
 
@@ -64,6 +63,9 @@
 qed  
 
 use "~~/src/Tools/Code/code_runtime.ML"
+use "~~/src/Tools/nbe.ML"
+
+setup Nbe.setup
 
 hide_const (open) holds