equal
deleted
inserted
replaced
12 if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ()) |
12 if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ()) |
13 then () |
13 then () |
14 else use "ML-Systems/single_assignment_polyml.ML"; |
14 else use "ML-Systems/single_assignment_polyml.ML"; |
15 |
15 |
16 use "ML-Systems/multithreading.ML"; |
16 use "ML-Systems/multithreading.ML"; |
17 use "General/timing.ML"; |
|
18 use "ML-Systems/ml_pretty.ML"; |
17 use "ML-Systems/ml_pretty.ML"; |
19 use "ML-Systems/use_context.ML"; |
18 use "ML-Systems/use_context.ML"; |
|
19 |
|
20 val seconds = Time.fromReal; |
|
21 |
20 |
22 |
21 |
23 |
22 (** ML system and platform related **) |
24 (** ML system and platform related **) |
23 |
25 |
24 val forget_structure = PolyML.Compiler.forgetStructure; |
26 val forget_structure = PolyML.Compiler.forgetStructure; |