src/Pure/ROOT.ML
changeset 62845 31177a9c3025
parent 62825 e6e80a8bf624
child 62846 3c576c7f9731
     1.1 --- a/src/Pure/ROOT.ML	Mon Apr 04 14:53:30 2016 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Mon Apr 04 15:35:24 2016 +0200
     1.3 @@ -11,13 +11,6 @@
     1.4  if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then ()
     1.5  else use "ML/fixed_int_dummy.ML";
     1.6  
     1.7 -structure Distribution =     (*filled-in by makedist*)
     1.8 -struct
     1.9 -  val version = "unidentified repository version";
    1.10 -  val is_identified = false;
    1.11 -  val is_official = false;
    1.12 -end;
    1.13 -
    1.14  
    1.15  (* multithreading *)
    1.16  
    1.17 @@ -29,6 +22,8 @@
    1.18  
    1.19  (* ML system *)
    1.20  
    1.21 +use "System/distribution.ML";
    1.22 +
    1.23  use "ML/ml_heap.ML";
    1.24  use "ML/ml_profiling.ML";
    1.25  use "ML/ml_pretty.ML";
    1.26 @@ -291,6 +286,7 @@
    1.27  else use "System/bash.ML";
    1.28  use "System/isabelle_system.ML";
    1.29  
    1.30 +
    1.31  (*theory documents*)
    1.32  use "Thy/term_style.ML";
    1.33  use "Isar/outer_syntax.ML";