diff -r d9794a370472 -r 8c0818fe58c7 src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Fri May 24 23:57:24 2013 +0200
+++ b/src/Tools/Code_Generator.thy	Fri May 24 23:57:24 2013 +0200
@@ -17,6 +17,7 @@
 ML_file "~~/src/Tools/value.ML"
 ML_file "~~/src/Tools/cache_io.ML"
 ML_file "~~/src/Tools/Code/code_preproc.ML"
+ML_file "~~/src/Tools/Code/code_symbol.ML"
 ML_file "~~/src/Tools/Code/code_thingol.ML"
 ML_file "~~/src/Tools/Code/code_simp.ML"
 ML_file "~~/src/Tools/Code/code_printer.ML"