# HG changeset patch
# User wenzelm
# Date 1230807636 -3600
# Node ID 4588e0070d4c9c01fe80b0188028b508b7df57a0
# Parent  f4743512b12d4d61af1660cd3258d1454122801f
isabelle-process;
provide structure Word;
provide IntInf.log2;

diff -r f4743512b12d -r 4588e0070d4c src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Thu Jan 01 10:42:48 2009 +0100
+++ b/src/Pure/ML-Systems/mosml.ML	Thu Jan 01 12:00:36 2009 +0100
@@ -1,14 +1,13 @@
 (*  Title:      Pure/ML-Systems/mosml.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1999  University of Cambridge
+    Author:     Makarius
 
 Compatibility file for Moscow ML 2.01
 
 NOTE: saving images does not work; may run it interactively as follows:
 
 $ cd Isabelle/src/Pure
-$ isabelle RAW_ML_SYSTEM
+$ isabelle-process RAW_ML_SYSTEM
 > val ml_system = "mosml";
 > use "ML-Systems/mosml.ML";
 > use "ROOT.ML";
@@ -27,6 +26,7 @@
 fun forget_structure _ = ();
 
 load "Obj";
+load "Word";
 load "Bool";
 load "Int";
 load "Real";
@@ -54,6 +54,14 @@
 structure IntInf =
 struct
   fun divMod (x, y) = (x div y, x mod y);
+
+  local
+    fun log 1 a = a
+      | log n a = log (n div 2) (a + 1);
+  in
+    fun log2 n = if n > 0 then log n 0 else raise Domain;
+  end;
+
   open Int;
 end;