tuned;

--- a/src/HOL/ROOT.ML	Thu Aug 26 19:04:19 1999 +0200
+++ b/src/HOL/ROOT.ML	Thu Aug 26 19:04:26 1999 +0200
@@ -15,6 +15,7 @@
 (*old-style theory syntax*)
 use "~~/src/Pure/section_utils.ML";
 use "thy_syntax.ML";
+
 use "hologic.ML";
 
 use "~~/src/Provers/simplifier.ML";
@@ -34,7 +35,6 @@
 
 use_thy "subset";
 use "Tools/typedef_package.ML";
-
 use_thy "Inductive";
 use_thy "NatDef";