# HG changeset patch
# User wenzelm
# Date 1233060752 -3600
# Node ID 08d462dbb1a9ded103c641d13aa04dd41073a5f8
# Parent  741f26190c96a542c5be03c5d723618b0c7fea2d# Parent  b9a7ea6c6da7c739604a7f22306167d848feee84
merged

diff -r 741f26190c96 -r 08d462dbb1a9 src/HOL/ROOT.ML
--- 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;
diff -r 741f26190c96 -r 08d462dbb1a9 src/Pure/ML-Systems/polyml-5.0.ML
--- 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;
+
diff -r 741f26190c96 -r 08d462dbb1a9 src/Pure/ML-Systems/polyml-5.1.ML
--- 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;
+
diff -r 741f26190c96 -r 08d462dbb1a9 src/Pure/ML-Systems/polyml.ML
--- 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 *)