| author | wenzelm |
| Mon, 24 Mar 2008 18:35:47 +0100 | |
| changeset 26381 | 509a1ca9d35c |
| child 26389 | 3835c431e141 |
| permissions | -rw-r--r-- |
(* Title: Pure/ML-Systems/polyml-5.1.ML ID: $Id$ Compatibility wrapper for Poly/ML 5.1. *) use "ML-Systems/polyml_common.ML"; use "ML-Systems/multithreading_polyml.ML"; val pointer_eq = PolyML.pointerEq; (* single-threaded profiling *) local val profile_orig = profile in fun profile 0 f x = f x | profile n f x = NAMED_CRITICAL "profile" (fn () => profile_orig n f x); end;