changeset 63932 | 6040db6b929d |
parent 63806 | c54a53ef1873 |
child 64304 | 96bc94c87a81 |
--- a/src/Pure/ROOT.ML Wed Sep 21 14:20:07 2016 +0100 +++ b/src/Pure/ROOT.ML Wed Sep 21 20:33:44 2016 +0200 @@ -10,6 +10,7 @@ ML_file "System/distribution.ML"; ML_file "General/basics.ML"; +ML_file "General/symbol_explode.ML"; ML_file "Concurrent/multithreading.ML"; ML_file "Concurrent/unsynchronized.ML";