src/Tools/Code_Generator.thy

 (*  Title:   Tools/Code_Generator.thy
     Author:  Florian Haftmann, TU Muenchen
 *)
 
-header {* Loading the code generator modules *}
+header {* Loading the code generator and related modules *}
 
 theory Code_Generator
 imports Pure
 uses
   "~~/src/Tools/cache_io.ML"

   "~~/src/Tools/Code/code_target.ML"
   "~~/src/Tools/Code/code_namespace.ML"
   "~~/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 {*
   Auto_Solve.setup
   #> Code_Preproc.setup
   #> Code_Simp.setup
   #> Code_ML.setup
   #> Code_Haskell.setup
   #> Code_Scala.setup
-  #> Nbe.setup
   #> Quickcheck.setup
 *}
 
 code_datatype "TYPE('a\<Colon>{})"
 

   show "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
     by rule (rule holds)+
 qed  
 
 use "~~/src/Tools/Code/code_runtime.ML"
+use "~~/src/Tools/nbe.ML"
+
+setup Nbe.setup
 
 hide_const (open) holds
 
 end