src/Pure/ML-Systems/polyml-5.1.ML
author wenzelm
Tue Mar 25 11:52:15 2008 +0100 (2008-03-25)
changeset 26389 3835c431e141
parent 26381 509a1ca9d35c
child 26390 99d4cbb1f941
permissions -rw-r--r--
use polyml_old_compiler5.ML;
     1 (*  Title:      Pure/ML-Systems/polyml-5.1.ML
     2     ID:         $Id$
     3 
     4 Compatibility wrapper for Poly/ML 5.1.
     5 *)
     6 
     7 use "ML-Systems/polyml_common.ML";
     8 use "ML-Systems/multithreading_polyml.ML";
     9 use "ML-Systems/polyml_old_compiler5.ML";
    10 
    11 val pointer_eq = PolyML.pointerEq;
    12 
    13 
    14 (* single-threaded profiling *)
    15 
    16 local val profile_orig = profile in
    17 
    18 fun profile 0 f x = f x
    19   | profile n f x = NAMED_CRITICAL "profile" (fn () => profile_orig n f x);
    20 
    21 end;