# HG changeset patch
# User wenzelm
# Date 921685553 -3600
# Node ID e2ecfd8622ae505cdd9929f41a52089c24f9ea50
# Parent  0da748358eff06f7a12ce725ae513aa71db74db5
tuned;

diff -r 0da748358eff -r e2ecfd8622ae src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Wed Mar 17 16:33:47 1999 +0100
+++ b/src/HOL/ROOT.ML	Wed Mar 17 16:45:53 1999 +0100
@@ -12,7 +12,7 @@
 
 print_depth 1;
 
-(* Add user sections *)
+(*old-style theory syntax*)
 use "~~/src/Pure/section_utils.ML";
 use "thy_syntax.ML";
 
@@ -56,8 +56,6 @@
 use "Tools/record_package.ML";
 use_thy "Record";
 
-use_thy "Arith";
-
 use_thy "Recdef";
 (*TFL: recursive function definitions*)
 cd "~~/src/TFL";