# HG changeset patch
# User wenzelm
# Date 1191271940 -7200
# Node ID 41a21f59f74d7ff38be4e47346b233b55ad021d2
# Parent  7c9a970d7ab52df752fe43624073e822d6c11e35
integer compatibility: added wrapper for structure Time;

diff -r 7c9a970d7ab5 -r 41a21f59f74d src/Pure/ML-Systems/alice.ML
--- 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);