equal
deleted
inserted
replaced
1 (* Title: Pure/ML/ml_pervasive.ML |
1 (* Title: Pure/ML/ml_pervasive.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Pervasive ML environment. |
4 Pervasive ML environment. |
5 *) |
5 *) |
|
6 |
|
7 structure PolyML_Pretty = |
|
8 struct |
|
9 datatype context = datatype PolyML.context; |
|
10 datatype pretty = datatype PolyML.pretty; |
|
11 end; |
6 |
12 |
7 val seconds = Time.fromReal; |
13 val seconds = Time.fromReal; |
8 |
14 |
9 val _ = |
15 val _ = |
10 List.app ML_Name_Space.forget_val |
16 List.app ML_Name_Space.forget_val |