src/Pure/ML-Systems/alice.ML
changeset 24809 41a21f59f74d
parent 24807 f66ab1dfbae1
child 26084 a7475459c740
--- a/src/Pure/ML-Systems/alice.ML	Mon Oct 01 22:29:58 2007 +0200
+++ b/src/Pure/ML-Systems/alice.ML	Mon Oct 01 22:52:20 2007 +0200
@@ -27,7 +27,16 @@
 (*low-level pointer equality*)
 fun pointer_eq (_: 'a, _: 'a) = false;
 
-(*downgraded IntInf*)
+
+(* integer compatibility -- downgraded IntInf *)
+
+structure Time =
+struct
+  open Time;
+  val fromMilliseconds = Time.fromMilliseconds o IntInf.fromInt;
+  val fromSeconds = Time.fromSeconds o IntInf.fromInt;
+end;
+
 structure IntInf =
 struct
   fun divMod (x, y) = (x div y, x mod y);