old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);

--- a/src/Pure/ML-Systems/polyml.ML	Fri Jul 19 17:58:57 2013 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Fri Jul 19 20:56:39 2013 +0200
@@ -58,6 +58,10 @@
 
 use "ML-Systems/ml_system.ML";
 
+if ML_System.name = "polyml-5.3.0"
+then use "ML-Systems/share_common_data_polyml-5.3.0.ML"
+else ();
+
 structure ML_System =
 struct
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/share_common_data_polyml-5.3.0.ML	Fri Jul 19 20:56:39 2013 +0200
@@ -0,0 +1,11 @@
+(*  Title:      Pure/ML-Systems/share_common_data_polyml-5.3.0.ML
+
+Dummy for Poly/ML 5.3.0, which cannot share the massive heap of HOL
+anymore.
+*)
+
+structure PolyML =
+struct
+  open PolyML;
+  fun shareCommonData _ = ();
+end;

--- a/src/Pure/ROOT	Fri Jul 19 17:58:57 2013 +0200
+++ b/src/Pure/ROOT	Fri Jul 19 20:56:39 2013 +0200
@@ -16,6 +16,7 @@
     "ML-Systems/proper_int.ML"
     "ML-Systems/single_assignment.ML"
     "ML-Systems/single_assignment_polyml.ML"
+    "ML-Systems/share_common_data_polyml-5.3.0.ML"
     "ML-Systems/smlnj.ML"
     "ML-Systems/thread_dummy.ML"
     "ML-Systems/universal.ML"