changeset 42012 | 2c3fe3cbebae |
parent 41718 | 05514b09bb4b |
child 42288 | 2074b31650e6 |
--- a/src/Pure/ML-Systems/polyml_common.ML Sun Mar 20 21:20:07 2011 +0100 +++ b/src/Pure/ML-Systems/polyml_common.ML Sun Mar 20 21:28:11 2011 +0100 @@ -14,10 +14,12 @@ else use "ML-Systems/single_assignment_polyml.ML"; use "ML-Systems/multithreading.ML"; -use "General/timing.ML"; use "ML-Systems/ml_pretty.ML"; use "ML-Systems/use_context.ML"; +val seconds = Time.fromReal; + + (** ML system and platform related **)