# HG changeset patch
# User wenzelm
# Date 1119132126 -7200
# Node ID 7e27422c603edebb0518388b7d9ca8d8d63cb42b
# Parent  452cd9ad3eda6bbf91f36e45a66bafc2edae0de6
some minor adaptions to make it work again;

diff -r 452cd9ad3eda -r 7e27422c603e src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Sat Jun 18 22:57:23 2005 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Sun Jun 19 00:02:06 2005 +0200
@@ -7,7 +7,7 @@
 
 NOTE: saving images does not work (yet!?), may run it interactively as follows:
 
-$ cd .../Pure
+$ cd ~~/src/Pure
 $ isabelle RAW_ML_SYSTEM
 > val ml_system = "mosml";
 > use "ML-Systems/mosml.ML";
@@ -16,29 +16,42 @@
 
 (** ML system related **)
 
-
 (* Poly/ML emulation *)
 
 load "Bool";
 load "Int";
 load "Real";
 load "ListPair";
-
 load "OS";
 load "Process";
 load "FileSys";
 
+(*proper implementation available?*)
+structure IntInf =
+struct
+  open Int;
+end;
+
+structure Real =
+struct
+  open Real;
+  val realFloor = real o floor;
+end;
+
+structure Time =
+struct
+  open Time;
+  fun toString t = Time.toString t
+    handle Overflow => Real.toString (Time.toReal t);   (*workaround Y2004 bug*)
+end;
+
 structure OS =
-  struct
+struct
   open OS
   structure Process = Process
   structure FileSys = FileSys
-  end;
+end;
  
-(*To exit the system with an exit code -- an alternative to ^D *)
-fun exit 0 = Process.exit Process.success
-  | exit _ = Process.exit Process.failure;
-
 (*limit the printing depth*)
 fun print_depth n =
  (Meta.printDepth := n div 2;