isabelle: src/Pure/ML-Systems/polyml-5.0.ML@40c3f900c457 (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
28151 61f9c918b410 explicit use of universal.ML and dummy_thread.ML; wenzelm parents: 26378 diff changeset	7	use "ML-Systems/universal.ML";
61f9c918b410 explicit use of universal.ML and dummy_thread.ML; wenzelm parents: 26378 diff changeset	8	use "ML-Systems/thread_dummy.ML";
26215 94d32a7cd0fb rearrangements to make latest Poly/ML the default, not old 4.x; wenzelm parents: 24605 diff changeset	9	use "ML-Systems/polyml_common.ML";
26378 bac8d5e5f833 moved use_text/file to polyml_old_compiler5.ML; wenzelm parents: 26215 diff changeset	10	use "ML-Systems/polyml_old_compiler5.ML";
21653 219924615db6 setup for polyml-5.0; wenzelm parents: diff changeset	11
219924615db6 setup for polyml-5.0; wenzelm parents: diff changeset	12	val pointer_eq = PolyML.pointerEq;
21771 148c8aba89dd added improved versions of use_text/file (still inactive); wenzelm parents: 21653 diff changeset	13