src/Pure/ML-Systems/polyml.ML

 
 Compatibility file for Poly/ML (version 4.1.x and 4.2.0).
 *)
 
 use "ML-Systems/exn.ML";
-use "ML-Systems/multithreading_dummy.ML";
+use "ML-Systems/multithreading.ML";
+use "ML-Systems/time_limit.ML";
 
 val ml_system_fix_ints = false;
 
 
 (** ML system and platform related **)

 fun check_timer timer =
   let
     val {sys, usr} = Timer.checkCPUTimer timer;
     val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
   in (sys, usr, gc) end;
-
-
-(* bounded time execution *)
-
-(*dummy implementation*)
-fun interrupt_timeout time f x =
-  f x;
 
 
 (* prompts *)
 
 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);