author | haftmann |
Mon, 16 Feb 2009 19:11:55 +0100 | |
changeset 29940 | 83b373f61d41 |
parent 29638 | 1f8f3d26a2cf |
child 30627 | fb9e73c01603 |
permissions | -rw-r--r-- |
(* Title: Pure/ML-Systems/polyml-5.0.ML Compatibility wrapper for Poly/ML 5.0. *) use "ML-Systems/universal.ML"; use "ML-Systems/thread_dummy.ML"; use "ML-Systems/polyml_common.ML"; use "ML-Systems/polyml_old_compiler5.ML"; val pointer_eq = PolyML.pointerEq; fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;