src/Pure/RAW/ml_heap_polyml-5.3.0.ML
changeset 62501 98fa1f9a292f
parent 62498 5dfcc9697f29
child 62502 8857237c3a90
--- a/src/Pure/RAW/ml_heap_polyml-5.3.0.ML	Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(*  Title:      Pure/RAW/ml_heap_polyml-5.3.0.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 () = ();
-  val save_state = PolyML.SaveState.saveState o ML_System.platform_path;
-end;