# HG changeset patch
# User wenzelm
# Date 1159479780 -7200
# Node ID 4eb07237382a1a238463626f49a740e12f7bfc1a
# Parent  f39c733f2a7e0d2f197dcfe4d316af73314e10ba
added share_data;

diff -r f39c733f2a7e -r 4eb07237382a src/Pure/ML-Systems/polyml-4.9.1.ML
--- a/src/Pure/ML-Systems/polyml-4.9.1.ML	Thu Sep 28 23:42:59 2006 +0200
+++ b/src/Pure/ML-Systems/polyml-4.9.1.ML	Thu Sep 28 23:43:00 2006 +0200
@@ -7,3 +7,5 @@
 
 use "ML-Systems/polyml-4.1.4-patch.ML";
 use "ML-Systems/polyml.ML";
+
+val share_data = SOME (fn x => (PolyML.shareCommonData x; x));