diff -r dd5f3a6fee73 -r 8e54fd480809 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Apr 04 20:20:47 2016 +0200
+++ b/src/Pure/ROOT.ML	Mon Apr 04 20:28:17 2016 +0200
@@ -4,9 +4,9 @@
 
 (* initial ML name space *)
 
-use "ML/ml_system.ML";
 use "ML/ml_name_space.ML";
 use "ML/ml_pervasive_initial.ML";
+use "ML/ml_system.ML";
 
 if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then ()
 else use "ML/fixed_int_dummy.ML";