1.1 --- a/src/Pure/ML-Systems/polyml-5.1.ML	Thu Oct 04 21:10:41 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/polyml-5.1.ML	Thu Oct 04 21:11:06 2007 +0200
     1.3 @@ -10,6 +10,16 @@
     1.4  val pointer_eq = PolyML.pointerEq;
     1.5  
     1.6  
     1.7 +(* single-threaded profiling *)
     1.8 +
     1.9 +local val profile_orig = profile in
    1.10 +
    1.11 +fun profile 0 f x = f x
    1.12 +  | profile n f x = NAMED_CRITICAL "profile" (fn () => profile_orig n f x);
    1.13 +
    1.14 +end;
    1.15 +
    1.16 +
    1.17  (* improved versions of use_text/file *)
    1.18  
    1.19  fun use_text (tune: string -> string) name (print, err) verbose txt =