src/Pure/RAW/ml_heap.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_heap.ML	Mon Feb 29 15:23:13 2016 +0100
@@ -0,0 +1,17 @@
+(*  Title:      Pure/RAW/ml_heap.ML
+    Author:     Makarius
+
+ML heap operations.
+*)
+
+signature ML_HEAP =
+sig
+  val share_common_data: unit -> unit
+  val save_state: string -> unit
+end;
+
+structure ML_Heap: ML_HEAP =
+struct
+  fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+  val save_state = PolyML.SaveState.saveState o ml_platform_path;
+end;