# HG changeset patch
# User paulson
# Date 849022170 -3600
# Node ID 275a5a699ff714d2427e79cf4b1987e2664ac43a
# Parent  64acb485eccef3cdd39acde0a5938f58a9e78913
Structure Bool and value Int.toString needed to replace makestring calls

diff -r 64acb485ecce -r 275a5a699ff7 src/Pure/basis.ML
--- a/src/Pure/basis.ML	Tue Nov 26 16:26:06 1996 +0100
+++ b/src/Pure/basis.ML	Tue Nov 26 16:29:30 1996 +0100
@@ -10,8 +10,15 @@
 Full compatibility cannot be obtained using a file: what about char constants?
 *)
 
+structure Bool =
+  struct
+  fun toString true  = "true"
+    | toString false = "false"
+  end;
+
 structure Int =
   struct
+  fun toString (i: int) = makestring i;
   fun max (x, y) = if x < y then y else x : int;
   fun min (x, y) = if x < y then x else y : int;
   end;