proper use_thy;
authorwenzelm
Tue Apr 05 17:16:46 2016 +0200 (2016-04-05)
changeset 6286964a5cf42be1e
parent 62868 61a691db1c4d
child 62870 cf724647f75b
proper use_thy;
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ROOT.ML	Tue Apr 05 15:58:58 2016 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Tue Apr 05 17:16:46 2016 +0200
     1.3 @@ -335,5 +335,6 @@
     1.4  use "Tools/jedit.ML";
     1.5  
     1.6  use_thy "Pure";
     1.7 +use_thy "ML/ML_Root";
     1.8  
     1.9  use "ML/ml_pervasive_final.ML";