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));