tuned comments;
authorwenzelm
Fri, 10 Nov 2006 00:12:28 +0100
changeset 21280 b4aa7daa506b
parent 21279 2cb5f1621bcf
child 21281 0767e7dad549
tuned comments;
src/Pure/ML-Systems/mosml.ML
src/Pure/ML-Systems/polyml-4.9.1.ML
--- 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