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;