changeset 62468 | d97e13e5ea5b |
parent 62467 | c1b88e647e2f |
child 62472 | 01e2bd5b4027 |
--- a/src/Pure/RAW/ROOT_polyml.ML Mon Feb 29 15:23:13 2016 +0100 +++ b/src/Pure/RAW/ROOT_polyml.ML Mon Feb 29 15:39:17 2016 +0100 @@ -31,11 +31,6 @@ (* ML heap operations *) -fun ml_platform_path (s: string) = s; -fun ml_standard_path (s: string) = s; - -if ML_System.platform_is_windows then use "RAW/windows_path.ML" else (); - if ML_System.name = "polyml-5.3.0" then use "RAW/ml_heap_polyml-5.3.0.ML" else use "RAW/ml_heap.ML";