--- a/src/Pure/ML-Systems/mosml.ML Thu Nov 09 23:40:19 2006 +0100
+++ b/src/Pure/ML-Systems/mosml.ML Fri Nov 10 00:12:28 2006 +0100
@@ -97,10 +97,11 @@
(* bounded time execution *)
-(* FIXME proper implementation available? *)
+(*dummy implementation*)
fun interrupt_timeout time f x =
f x;
+
(* ML command execution *)
(*Can one redirect 'use' directly to an instream?*)
--- a/src/Pure/ML-Systems/polyml-4.9.1.ML Thu Nov 09 23:40:19 2006 +0100
+++ b/src/Pure/ML-Systems/polyml-4.9.1.ML Fri Nov 10 00:12:28 2006 +0100
@@ -1,4 +1,4 @@
-(* Title: Pure/ML-Systems/polyml-4.2.0.ML
+(* Title: Pure/ML-Systems/polyml-4.9.1.ML
ID: $Id$
Author: Makarius