# HG changeset patch # User wenzelm # Date 1184879930 -7200 # Node ID 365682a666da8155a2bcfb5c2a33d2b087af9532 # Parent 8f3099589cfabc4f3dfadc867934ec32945a0650 use thy_header.ML earlier; diff -r 8f3099589cfa -r 365682a666da src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Thu Jul 19 23:18:48 2007 +0200 +++ b/src/Pure/Isar/ROOT.ML Thu Jul 19 23:18:50 2007 +0200 @@ -23,6 +23,7 @@ (*theory sources*) use "../Thy/ml_context.ML"; +use "../Thy/thy_header.ML"; use "../Thy/thy_load.ML"; use "../Thy/thy_info.ML"; use "../Thy/html.ML"; @@ -67,7 +68,6 @@ use "../Thy/thy_output.ML"; (*theory syntax*) -use "../Thy/thy_header.ML"; use "session.ML"; use "../old_goals.ML"; use "outer_syntax.ML";