more operations;

--- 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 =