src/Pure/ML/ml_pervasive0.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_pervasive0.ML	Wed Apr 06 11:37:37 2016 +0200
@@ -0,0 +1,28 @@
+(*  Title:      Pure/ML/ml_pervasive0.ML
+    Author:     Makarius
+
+Pervasive ML environment: initial setup.
+*)
+
+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;