src/Pure/ML-Systems/polyml.ML
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;