diff -r 33638f4883ac -r 1986f18c4940 src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Thu Sep 16 16:51:34 2010 +0200
+++ b/src/Tools/Code_Generator.thy	Thu Sep 16 16:51:34 2010 +0200
@@ -21,8 +21,8 @@
   "~~/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/nbe.ML"
+  ("~~/src/Tools/Code/code_runtime.ML")
 begin
 
 setup {*
@@ -32,7 +32,6 @@
   #> Code_ML.setup
   #> Code_Haskell.setup
   #> Code_Scala.setup
-  #> Code_Runtime.setup
   #> Nbe.setup
   #> Quickcheck.setup
 *}
@@ -64,6 +63,8 @@
     by rule (rule holds)+
 qed  
 
+use "~~/src/Tools/Code/code_runtime.ML"
+
 hide_const (open) holds
 
 end