added share_common_data -- reduces heap space, but takes long;

--- a/src/HOL/ROOT.ML	Tue Jan 27 00:42:12 2009 +0100
+++ b/src/HOL/ROOT.ML	Tue Jan 27 12:59:22 2009 +0100
@@ -1,6 +1,7 @@
 (* Classical Higher-order Logic -- batteries included *)
 
 use_thy "Main";
+share_common_data ();
 use_thy "Complex_Main";
 
 val HOL_proofs = ! Proofterm.proofs;

--- a/src/Pure/ML-Systems/polyml-5.0.ML	Tue Jan 27 00:42:12 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-5.0.ML	Tue Jan 27 12:59:22 2009 +0100
@@ -10,3 +10,5 @@
 
 val pointer_eq = PolyML.pointerEq;
 
+fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+

--- a/src/Pure/ML-Systems/polyml-5.1.ML	Tue Jan 27 00:42:12 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-5.1.ML	Tue Jan 27 12:59:22 2009 +0100
@@ -8,3 +8,6 @@
 use "ML-Systems/polyml_old_compiler5.ML";
 
 val pointer_eq = PolyML.pointerEq;
+
+fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+

--- a/src/Pure/ML-Systems/polyml.ML	Tue Jan 27 00:42:12 2009 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Jan 27 12:59:22 2009 +0100
@@ -12,6 +12,8 @@
 
 val pointer_eq = PolyML.pointerEq;
 
+fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+
 
 (* runtime compilation *)