| author | blanchet |
| Wed, 24 Sep 2014 15:45:55 +0200 | |
| changeset 58425 | 246985c6b20b |
| parent 52711 | 155f02cacb2d |
| permissions | -rw-r--r-- |
|
52711
155f02cacb2d
old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/share_common_data_polyml-5.3.0.ML |
|
155f02cacb2d
old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);
wenzelm
parents:
diff
changeset
|
2 |
|
|
155f02cacb2d
old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);
wenzelm
parents:
diff
changeset
|
3 |
Dummy for Poly/ML 5.3.0, which cannot share the massive heap of HOL |
|
155f02cacb2d
old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);
wenzelm
parents:
diff
changeset
|
4 |
anymore. |
|
155f02cacb2d
old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);
wenzelm
parents:
diff
changeset
|
5 |
*) |
|
155f02cacb2d
old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);
wenzelm
parents:
diff
changeset
|
6 |
|
|
155f02cacb2d
old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);
wenzelm
parents:
diff
changeset
|
7 |
structure PolyML = |
|
155f02cacb2d
old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);
wenzelm
parents:
diff
changeset
|
8 |
struct |
|
155f02cacb2d
old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);
wenzelm
parents:
diff
changeset
|
9 |
open PolyML; |
|
155f02cacb2d
old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);
wenzelm
parents:
diff
changeset
|
10 |
fun shareCommonData _ = (); |
|
155f02cacb2d
old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);
wenzelm
parents:
diff
changeset
|
11 |
end; |