changeset 60967 | eb87fc42825c |
parent 60965 | 49c797cb9f46 |
child 60993 | 531a48ae1425 |
--- a/src/Pure/ML-Systems/polyml.ML Tue Aug 18 14:28:29 2015 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Tue Aug 18 14:43:25 2015 +0200 @@ -38,12 +38,9 @@ structure ML_System = struct - -open ML_System; - -fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; -val save_state = PolyML.SaveState.saveState; - + open ML_System; + fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; + val save_state = PolyML.SaveState.saveState o ml_platform_path; end;