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

--- a/src/Pure/ML-Systems/share_common_data_polyml-5.3.0.ML	Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-(*  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;