eliminated misleading dummy versions of print/makestring, cf. 6974449ddea9;
authorwenzelm
Sun May 31 17:47:04 2009 +0200 (2009-05-31)
changeset 31321fe786d4633b9
parent 31320 72eeb1b4e006
child 31322 526e149999cc
eliminated misleading dummy versions of print/makestring, cf. 6974449ddea9;
src/Pure/ML-Systems/mosml.ML
src/Pure/ML-Systems/smlnj.ML
     1.1 --- a/src/Pure/ML-Systems/mosml.ML	Sun May 31 17:45:53 2009 +0200
     1.2 +++ b/src/Pure/ML-Systems/mosml.ML	Sun May 31 17:47:04 2009 +0200
     1.3 @@ -132,8 +132,6 @@
     1.4  (*dummy implementation*)
     1.5  fun exception_trace f = f ();
     1.6  
     1.7 -(*dummy implementation*)
     1.8 -fun print x = x;
     1.9  
    1.10  
    1.11  (** Compiler-independent timing functions **)
     2.1 --- a/src/Pure/ML-Systems/smlnj.ML	Sun May 31 17:45:53 2009 +0200
     2.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Sun May 31 17:47:04 2009 +0200
     2.3 @@ -92,12 +92,6 @@
     2.4  (*dummy implementation*)
     2.5  fun exception_trace f = f ();
     2.6  
     2.7 -(*dummy implementation*)
     2.8 -fun print x = x;
     2.9 -
    2.10 -(*dummy implementation*)
    2.11 -fun makestring x = "dummy string for SML New Jersey";
    2.12 -
    2.13  
    2.14  (* ML command execution *)
    2.15