--- a/src/HOL/ROOT.ML Tue Jan 27 13:41:45 2009 +0100
+++ b/src/HOL/ROOT.ML Tue Jan 27 13:52:32 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 13:41:45 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-5.0.ML Tue Jan 27 13:52:32 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 13:41:45 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-5.1.ML Tue Jan 27 13:52:32 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 13:41:45 2009 +0100
+++ b/src/Pure/ML-Systems/polyml.ML Tue Jan 27 13:52:32 2009 +0100
@@ -12,6 +12,8 @@
val pointer_eq = PolyML.pointerEq;
+fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+
(* runtime compilation *)