# HG changeset patch
# User wenzelm
# Date 1460316648 -7200
# Node ID 659a8737501d6848bf68ee1506541f4144d67d6c
# Parent  ba10c4e226cf50eb4094d4aa092a68e2cd18ecf7
clarified files;

diff -r ba10c4e226cf -r 659a8737501d src/Pure/ML/ml_pervasive.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_pervasive.ML	Sun Apr 10 21:30:48 2016 +0200
@@ -0,0 +1,33 @@
+(*  Title:      Pure/ML/ml_pervasive.ML
+    Author:     Makarius
+
+Initial 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;
+
+datatype illegal = Interrupt;
+
+structure Basic_Exn: BASIC_EXN = Exn;
+open Basic_Exn;
diff -r ba10c4e226cf -r 659a8737501d src/Pure/ML/ml_pervasive0.ML
--- a/src/Pure/ML/ml_pervasive0.ML	Sun Apr 10 20:15:39 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(*  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;
-
-datatype illegal = Interrupt;
-
-structure Basic_Exn: BASIC_EXN = Exn;
-open Basic_Exn;
diff -r ba10c4e226cf -r 659a8737501d src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sun Apr 10 20:15:39 2016 +0200
+++ b/src/Pure/ROOT.ML	Sun Apr 10 21:30:48 2016 +0200
@@ -5,7 +5,7 @@
 
 section "Bootstrap phase 0: Poly/ML setup";
 
-ML_file "ML/ml_pervasive0.ML";
+ML_file "ML/ml_pervasive.ML";
 ML_file "ML/ml_system.ML";
 ML_file "System/distribution.ML";