--- a/src/HOL/ROOT.ML Wed Oct 19 21:52:30 2005 +0200
+++ b/src/HOL/ROOT.ML Wed Oct 19 21:52:31 2005 +0200
@@ -9,9 +9,6 @@
val banner = "Higher-Order Logic";
writeln banner;
-(*old-style theory syntax*)
-use "thy_syntax.ML";
-
use "hologic.ML";
use "~~/src/Provers/splitter.ML";