src/Pure/RAW/share_common_data_polyml-5.3.0.ML
changeset 61925 ab52f183f020
parent 52711 155f02cacb2d
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/share_common_data_polyml-5.3.0.ML	Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,11 @@
+(*  Title:      Pure/RAW/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;