# HG changeset patch
# User wenzelm
# Date 977505900 -3600
# Node ID bbaa0c6ef59ff30a67f4863c70ef2aa1be76a56d
# Parent  1b3350c4ee92a0e7deee951ceb34651d065ba2e8
SML90 stuff;

diff -r 1b3350c4ee92 -r bbaa0c6ef59f src/Pure/ML-Systems/mlworks.ML
--- a/src/Pure/ML-Systems/mlworks.ML	Fri Dec 22 18:24:39 2000 +0100
+++ b/src/Pure/ML-Systems/mlworks.ML	Fri Dec 22 18:25:00 2000 +0100
@@ -10,10 +10,10 @@
 
 (* restore old-style character / string functions *)
 
-fun ord s = Char.ord (String.sub (s, 0));
-val chr = str o Char.chr;
-val explode = (map str) o String.explode;
-val implode = String.concat;
+val ord = SML90.ord;
+val chr = SML90.chr;
+val explode = SML90.explode;
+val implode = SML90.implode;
 
 
 (* MLWorks parameters *)