added dummy makestring function
authorobua
Wed Jul 11 11:47:59 2007 +0200 (2007-07-11)
changeset 237702711e0285072
parent 23769 7bc32680a495
child 23771 bde6db239efa
added dummy makestring function
src/Pure/ML-Systems/smlnj.ML
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Jul 11 11:47:24 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed Jul 11 11:47:59 2007 +0200
     1.3 @@ -77,6 +77,9 @@
     1.4  (*dummy implementation*)
     1.5  fun print x = x;
     1.6  
     1.7 +(*dummy implementation*)
     1.8 +fun makestring x = "dummy string for SML New Jersey";
     1.9 +
    1.10  
    1.11  (* toplevel pretty printing (see also Pure/install_pp.ML) *)
    1.12