# HG changeset patch
# User wenzelm
# Date 1191270596 -7200
# Node ID f66ab1dfbae1ca6ebc77b58ae30b7012007953b1
# Parent  c070cd2a145067429e89621d731894cd0b0c734a
downgraded IntInf with divMod;
fixed use_text;

diff -r c070cd2a1450 -r f66ab1dfbae1 src/Pure/ML-Systems/alice.ML
--- a/src/Pure/ML-Systems/alice.ML	Mon Oct 01 21:19:54 2007 +0200
+++ b/src/Pure/ML-Systems/alice.ML	Mon Oct 01 22:29:56 2007 +0200
@@ -8,6 +8,9 @@
 $ cd Isabelle/src/Pure
 $ env ALICE_JIT_MODE=0 alice
 - val ml_system = "alice";
+- use "ML-Systems/exn.ML";
+- use "ML-Systems/multithreading.ML";
+- use "ML-Systems/time_limit.ML";
 - use "ML-Systems/alice.ML";
 - use "ROOT.ML";
 - Session.finish ();
@@ -15,11 +18,6 @@
 
 val ml_system_fix_ints = false;
 
-use "ML-Systems/exn.ML";
-use "ML-Systems/multithreading.ML";
-use "ML-Systems/time_limit.ML";
-
-
 fun exit 0 = (OS.Process.exit OS.Process.success): unit
   | exit _ = OS.Process.exit OS.Process.failure;
 
@@ -29,6 +27,13 @@
 (*low-level pointer equality*)
 fun pointer_eq (_: 'a, _: 'a) = false;
 
+(*downgraded IntInf*)
+structure IntInf =
+struct
+  fun divMod (x, y) = (x div y, x mod y);
+  open Int;
+end;
+
 
 (* restore old-style character / string functions *)
 
@@ -102,9 +107,9 @@
 
 (* ML command execution *)
 
-fun use_text name (print, err) verbose txt = (Compiler.eval txt; ());
+fun use_text tune name (print, err) verbose txt = (Compiler.eval txt; ());
 
-fun use_file _ _ name = use name;
+fun use_file tune output verbose name = use name;