equal
deleted
inserted
replaced
94 then use "ML/exn_properties_polyml.ML" |
94 then use "ML/exn_properties_polyml.ML" |
95 else use "ML/exn_properties_dummy.ML"; |
95 else use "ML/exn_properties_dummy.ML"; |
96 |
96 |
97 if ML_System.name = "polyml-5.5.1" |
97 if ML_System.name = "polyml-5.5.1" |
98 orelse ML_System.name = "polyml-5.5.2" |
98 orelse ML_System.name = "polyml-5.5.2" |
|
99 orelse ML_System.name = "polyml-5.5.3" |
99 then use "ML/exn_trace_polyml-5.5.1.ML" |
100 then use "ML/exn_trace_polyml-5.5.1.ML" |
100 else (); |
101 else (); |
101 |
102 |
102 if ML_System.name = "polyml-5.5.0" |
103 if ML_System.name = "polyml-5.5.0" |
103 orelse ML_System.name = "polyml-5.5.1" |
104 orelse ML_System.name = "polyml-5.5.1" |
104 orelse ML_System.name = "polyml-5.5.2" |
105 orelse ML_System.name = "polyml-5.5.2" |
|
106 orelse ML_System.name = "polyml-5.5.3" |
105 then use "ML/ml_statistics_polyml-5.5.0.ML" |
107 then use "ML/ml_statistics_polyml-5.5.0.ML" |
106 else use "ML/ml_statistics_dummy.ML"; |
108 else use "ML/ml_statistics_dummy.ML"; |
107 |
109 |
108 use "Concurrent/single_assignment.ML"; |
110 use "Concurrent/single_assignment.ML"; |
109 if Multithreading.available then () |
111 if Multithreading.available then () |