# HG changeset patch
# User obua
# Date 1184147279 -7200
# Node ID 2711e0285072e4819b270c7acaa88c4e4787b45b
# Parent  7bc32680a4952ad76d999feb9ff55249ee0adeb7
added dummy makestring function

diff -r 7bc32680a495 -r 2711e0285072 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Wed Jul 11 11:47:24 2007 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Jul 11 11:47:59 2007 +0200
@@ -77,6 +77,9 @@
 (*dummy implementation*)
 fun print x = x;
 
+(*dummy implementation*)
+fun makestring x = "dummy string for SML New Jersey";
+
 
 (* toplevel pretty printing (see also Pure/install_pp.ML) *)