changeset 40393 | 2bb7ec08574a |
parent 39616 | 8052101883c3 |
child 40627 | becf5d5187cc |
--- a/src/Pure/ML-Systems/polyml_common.ML Sat Nov 06 16:53:07 2010 +0100 +++ b/src/Pure/ML-Systems/polyml_common.ML Sat Nov 06 17:55:32 2010 +0100 @@ -13,7 +13,7 @@ use "ML-Systems/multithreading.ML"; use "ML-Systems/time_limit.ML"; -use "ML-Systems/timing.ML"; +use "General/timing.ML"; use "ML-Systems/bash.ML"; use "ML-Systems/ml_pretty.ML"; use "ML-Systems/use_context.ML";