--- a/src/Pure/ML/ml_pervasive.ML Mon Apr 04 20:07:08 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(* Title: Pure/ML/ml_pervasive.ML
- Author: Makarius
-
-Pervasive ML environment.
-*)
-
-structure PolyML_Pretty =
-struct
- datatype context = datatype PolyML.context;
- datatype pretty = datatype PolyML.pretty;
-end;
-
-val seconds = Time.fromReal;
-
-val _ =
- List.app ML_Name_Space.forget_val
- ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
-
-val ord = SML90.ord;
-val chr = SML90.chr;
-val raw_explode = SML90.explode;
-val implode = SML90.implode;
-
-val pointer_eq = PolyML.pointerEq;
-
-val error_depth = PolyML.error_depth;
-
-open Thread;