| changeset 52711 | 155f02cacb2d |
| parent 51638 | 1275716f395b |
| child 52837 | fe1f6a1707f7 |
--- 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