author | wenzelm |
Fri, 16 Feb 2018 14:10:37 +0100 | |
changeset 67622 | 5289d3bdb261 |
parent 67621 | 8f93d878f855 |
child 67623 | dee9d2924617 |
--- a/src/Pure/ML/ml_heap.ML Thu Feb 15 17:08:25 2018 +0100 +++ b/src/Pure/ML/ml_heap.ML Fri Feb 16 14:10:37 2018 +0100 @@ -7,6 +7,7 @@ signature ML_HEAP = sig val obj_size: 'a -> int + val full_gc: unit -> unit val share_common_data: unit -> unit val save_child: string -> unit end; @@ -16,6 +17,8 @@ val obj_size = PolyML.objSize; +val full_gc = PolyML.fullGC; + fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; fun save_child name =