# HG changeset patch # User wenzelm # Date 1187090415 -7200 # Node ID 15a43b49487895cc7bd3f31416082acdf735d30b # Parent 21919609a1c076658e740b6e9871c4055356920f use logic.ML earlier; added primitive_defs.ML; diff -r 21919609a1c0 -r 15a43b494878 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Aug 14 13:20:14 2007 +0200 +++ b/src/Pure/ROOT.ML Tue Aug 14 13:20:15 2007 +0200 @@ -22,6 +22,7 @@ use "name.ML"; use "term.ML"; use "term_subst.ML"; +use "logic.ML"; use "General/pretty.ML"; use "Syntax/lexicon.ML"; use "Syntax/simple_syntax.ML"; @@ -47,8 +48,8 @@ (*core of tactical proof system*) use "envir.ML"; -use "logic.ML"; use "consts.ML"; +use "primitive_defs.ML"; use "sign.ML"; use "pattern.ML"; use "unify.ML";