diff -r 9019b6afaa4a -r 9969401e1fb8 src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Wed Sep 15 16:56:31 2010 +0200
+++ b/src/Tools/Code_Generator.thy	Wed Sep 15 16:56:31 2010 +0200
@@ -21,10 +21,22 @@
   "~~/src/Tools/Code/code_ml.ML"
   "~~/src/Tools/Code/code_haskell.ML"
   "~~/src/Tools/Code/code_scala.ML"
-  ("~~/src/Tools/Code/code_runtime.ML")
+  "~~/src/Tools/Code/code_runtime.ML"
   "~~/src/Tools/nbe.ML"
 begin
 
+setup {*
+  Auto_Solve.setup
+  #> Code_Preproc.setup
+  #> Code_Simp.setup
+  #> Code_ML.setup
+  #> Code_Haskell.setup
+  #> Code_Scala.setup
+  #> Code_Runtime.setup
+  #> Nbe.setup
+  #> Quickcheck.setup
+*}
+
 code_datatype "TYPE('a\<Colon>{})"
 
 definition holds :: "prop" where
@@ -52,20 +64,6 @@
     by rule (rule holds)+
 qed  
 
-use "~~/src/Tools/Code/code_runtime.ML"
-
-setup {*
-  Auto_Solve.setup
-  #> Code_Preproc.setup
-  #> Code_Simp.setup
-  #> Code_ML.setup
-  #> Code_Haskell.setup
-  #> Code_Scala.setup
-  #> Code_Runtime.setup
-  #> Nbe.setup
-  #> Quickcheck.setup
-*}
-
 hide_const (open) holds
 
 end