| changeset 52136 | 8c0818fe58c7 |
| parent 51275 | 3928173409e4 |
| child 52137 | 7f7337447b1b |
--- 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"