eliminated misleading dummy versions of print/makestring, cf. 6974449ddea9;
authorwenzelm
Sun, 31 May 2009 17:47:04 +0200
changeset 31321 fe786d4633b9
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
--- a/src/Pure/ML-Systems/mosml.ML	Sun May 31 17:45:53 2009 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Sun May 31 17:47:04 2009 +0200
@@ -132,8 +132,6 @@
 (*dummy implementation*)
 fun exception_trace f = f ();
 
-(*dummy implementation*)
-fun print x = x;
 
 
 (** Compiler-independent timing functions **)
--- a/src/Pure/ML-Systems/smlnj.ML	Sun May 31 17:45:53 2009 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Sun May 31 17:47:04 2009 +0200
@@ -92,12 +92,6 @@
 (*dummy implementation*)
 fun exception_trace f = f ();
 
-(*dummy implementation*)
-fun print x = x;
-
-(*dummy implementation*)
-fun makestring x = "dummy string for SML New Jersey";
-
 
 (* ML command execution *)