integer compatibility: added wrapper for structure Time;
authorwenzelm
Mon Oct 01 22:52:20 2007 +0200 (2007-10-01)
changeset 2480941a21f59f74d
parent 24808 7c9a970d7ab5
child 24810 862b71696efe
integer compatibility: added wrapper for structure Time;
src/Pure/ML-Systems/alice.ML
     1.1 --- a/src/Pure/ML-Systems/alice.ML	Mon Oct 01 22:29:58 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/alice.ML	Mon Oct 01 22:52:20 2007 +0200
     1.3 @@ -27,7 +27,16 @@
     1.4  (*low-level pointer equality*)
     1.5  fun pointer_eq (_: 'a, _: 'a) = false;
     1.6  
     1.7 -(*downgraded IntInf*)
     1.8 +
     1.9 +(* integer compatibility -- downgraded IntInf *)
    1.10 +
    1.11 +structure Time =
    1.12 +struct
    1.13 +  open Time;
    1.14 +  val fromMilliseconds = Time.fromMilliseconds o IntInf.fromInt;
    1.15 +  val fromSeconds = Time.fromSeconds o IntInf.fromInt;
    1.16 +end;
    1.17 +
    1.18  structure IntInf =
    1.19  struct
    1.20    fun divMod (x, y) = (x div y, x mod y);