isabelle: src/Pure/ML-Systems/polyml-5.0.ML@27a8ad9612a3 (annotated)

21653 219924615db6 setup for polyml-5.0; wenzelm parents: diff changeset	1	(* Title: Pure/ML-Systems/polyml-5.0.ML
219924615db6 setup for polyml-5.0; wenzelm parents: diff changeset	2	ID: $Id$
219924615db6 setup for polyml-5.0; wenzelm parents: diff changeset	3
219924615db6 setup for polyml-5.0; wenzelm parents: diff changeset	4	Compatibility wrapper for Poly/ML 5.0.
219924615db6 setup for polyml-5.0; wenzelm parents: diff changeset	5	*)
219924615db6 setup for polyml-5.0; wenzelm parents: diff changeset	6
26215 94d32a7cd0fb rearrangements to make latest Poly/ML the default, not old 4.x; wenzelm parents: 24605 diff changeset	7	use "ML-Systems/polyml_common.ML";
26378 bac8d5e5f833 moved use_text/file to polyml_old_compiler5.ML; wenzelm parents: 26215 diff changeset	8	use "ML-Systems/polyml_old_compiler5.ML";
21653 219924615db6 setup for polyml-5.0; wenzelm parents: diff changeset	9
219924615db6 setup for polyml-5.0; wenzelm parents: diff changeset	10	val pointer_eq = PolyML.pointerEq;
21771 148c8aba89dd added improved versions of use_text/file (still inactive); wenzelm parents: 21653 diff changeset	11