src/Pure/ML-Systems/share_common_data_polyml-5.3.0.ML

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