--- a/src/Pure/ML-Systems/polyml.ML Sun Sep 23 23:39:42 2007 +0200
+++ b/src/Pure/ML-Systems/polyml.ML Mon Sep 24 13:52:50 2007 +0200
@@ -5,7 +5,8 @@
*)
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;
@@ -60,13 +61,6 @@
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);