--- a/src/Pure/ML-Systems/polyml.ML Sat Jul 21 10:55:42 2012 +0200
+++ b/src/Pure/ML-Systems/polyml.ML Sat Jul 21 12:42:28 2012 +0200
@@ -70,10 +70,20 @@
fun quit () = exit 0;
-(* ML system identification *)
+(* ML system operations *)
use "ML-Systems/ml_system.ML";
+structure ML_System =
+struct
+
+open ML_System;
+
+fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+val save_state = PolyML.SaveState.saveState;
+
+end;
+
(* ML runtime system *)
@@ -91,8 +101,6 @@
val pointer_eq = PolyML.pointerEq;
-fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-
(* ML compiler *)