equal
deleted
inserted
replaced
7 |
7 |
8 (** ML system related **) |
8 (** ML system related **) |
9 |
9 |
10 (* restore old-style character / string functions *) |
10 (* restore old-style character / string functions *) |
11 |
11 |
12 fun ord s = Char.ord (String.sub (s, 0)); |
12 val ord = SML90.ord; |
13 val chr = str o Char.chr; |
13 val chr = SML90.chr; |
14 val explode = (map str) o String.explode; |
14 val explode = SML90.explode; |
15 val implode = String.concat; |
15 val implode = SML90.implode; |
16 |
16 |
17 |
17 |
18 (* New Jersey ML parameters *) |
18 (* New Jersey ML parameters *) |
19 |
19 |
20 val _ = |
20 val _ = |