use logic.ML earlier;
authorwenzelm
Tue Aug 14 13:20:15 2007 +0200 (2007-08-14)
changeset 2425715a43b494878
parent 24256 21919609a1c0
child 24258 2f399483535a
use logic.ML earlier;
added primitive_defs.ML;
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ROOT.ML	Tue Aug 14 13:20:14 2007 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Tue Aug 14 13:20:15 2007 +0200
     1.3 @@ -22,6 +22,7 @@
     1.4  use "name.ML";
     1.5  use "term.ML";
     1.6  use "term_subst.ML";
     1.7 +use "logic.ML";
     1.8  use "General/pretty.ML";
     1.9  use "Syntax/lexicon.ML";
    1.10  use "Syntax/simple_syntax.ML";
    1.11 @@ -47,8 +48,8 @@
    1.12  
    1.13  (*core of tactical proof system*)
    1.14  use "envir.ML";
    1.15 -use "logic.ML";
    1.16  use "consts.ML";
    1.17 +use "primitive_defs.ML";
    1.18  use "sign.ML";
    1.19  use "pattern.ML";
    1.20  use "unify.ML";