--- 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