src/Pure/ROOT.ML
changeset 21475 ec0d1cf0eb35
parent 21396 afd8ba74313c
child 21640 9811f1560d38
     1.1 --- a/src/Pure/ROOT.ML	Thu Nov 23 00:51:51 2006 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Thu Nov 23 00:51:54 2006 +0100
     1.3 @@ -32,6 +32,7 @@
     1.4  
     1.5  (*inner syntax module*)
     1.6  cd "Syntax"; use "ROOT.ML"; cd "..";
     1.7 +use "General/ml_syntax.ML";
     1.8  
     1.9  (*core of tactical proof system*)
    1.10  use "envir.ML";
    1.11 @@ -46,6 +47,7 @@
    1.12  use "theory.ML";
    1.13  use "proofterm.ML";
    1.14  use "thm.ML";
    1.15 +use "morphism.ML";
    1.16  use "fact_index.ML";
    1.17  use "pure_thy.ML";
    1.18  use "display.ML";