# HG changeset patch
# User oheimb
# Date 902929114 -7200
# Node ID 81716d9b2b09c02aff43a68a766ea58b47bd5558
# Parent  410417e0fd04d2e3ffe456b23699d64cc66d130f
removed use_thys implied by use_thy "Main"

diff -r 410417e0fd04 -r 81716d9b2b09 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Wed Aug 12 15:31:35 1998 +0200
+++ b/src/HOL/ROOT.ML	Wed Aug 12 15:38:34 1998 +0200
@@ -56,12 +56,8 @@
 use_thy "Arith";
 use "arith_data.ML";
 
-use_thy "RelPow";
 use_thy "Finite";
-use_thy "Sexp";
-use_thy "Recdef";
 use_thy "Map";
-use_thy "Update";
 
 cd "Integ";
 use_thy "Bin";