author | wenzelm |
Sat, 02 Apr 2016 20:33:34 +0200 | |
changeset 62818 | 2733b240bfea |
child 62823 | 751bcf0473a7 |
permissions | -rw-r--r-- |
62818 | 1 |
(* Title: Pure/ML/ml_pervasive.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Pervasive ML environment. |
|
5 |
*) |
|
6 |
||
7 |
val seconds = Time.fromReal; |
|
8 |
||
9 |
val _ = |
|
10 |
List.app ML_Name_Space.forget_val |
|
11 |
["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"]; |
|
12 |
||
13 |
val ord = SML90.ord; |
|
14 |
val chr = SML90.chr; |
|
15 |
val raw_explode = SML90.explode; |
|
16 |
val implode = SML90.implode; |
|
17 |
||
18 |
val pointer_eq = PolyML.pointerEq; |
|
19 |
||
20 |
val error_depth = PolyML.error_depth; |
|
21 |
||
22 |
open Thread; |