--- a/src/Pure/ROOT.ML Tue Apr 05 18:20:25 2016 +0200 +++ b/src/Pure/ROOT.ML Tue Apr 05 18:25:42 2016 +0200 @@ -335,6 +335,6 @@ use "Tools/jedit.ML"; use_thy "Pure"; -use_thy "ML/ML_Root"; use "ML/ml_pervasive_final.ML"; +use_thy "ML/ML_Root";