# HG changeset patch
# User wenzelm
# Date 1233057578 -3600
# Node ID b9a7ea6c6da7c739604a7f22306167d848feee84
# Parent  da018485b89d4d8a786e15ac055311506773cca4# Parent  1f8f3d26a2cf0e496a9563cd539f9fccb8a722cc
merged

diff -r da018485b89d -r b9a7ea6c6da7 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Tue Jan 27 12:57:24 2009 +0100
+++ b/src/HOL/ROOT.ML	Tue Jan 27 12:59:38 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 da018485b89d -r b9a7ea6c6da7 src/Pure/ML-Systems/polyml-5.0.ML
--- a/src/Pure/ML-Systems/polyml-5.0.ML	Tue Jan 27 12:57:24 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-5.0.ML	Tue Jan 27 12:59:38 2009 +0100
@@ -10,3 +10,5 @@
 
 val pointer_eq = PolyML.pointerEq;
 
+fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+
diff -r da018485b89d -r b9a7ea6c6da7 src/Pure/ML-Systems/polyml-5.1.ML
--- a/src/Pure/ML-Systems/polyml-5.1.ML	Tue Jan 27 12:57:24 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-5.1.ML	Tue Jan 27 12:59:38 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 da018485b89d -r b9a7ea6c6da7 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Tue Jan 27 12:57:24 2009 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Jan 27 12:59:38 2009 +0100
@@ -12,6 +12,8 @@
 
 val pointer_eq = PolyML.pointerEq;
 
+fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+
 
 (* runtime compilation *)