# HG changeset patch
# User wenzelm
# Date 1518786637 -3600
# Node ID 5289d3bdb2615220c63c45d0c31dc72b05393e0b
# Parent  8f93d878f8552743905cd973718d7ccdf5c3c18c
more operations;

diff -r 8f93d878f855 -r 5289d3bdb261 src/Pure/ML/ml_heap.ML
--- 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 =