diff -r 6e805f389355 -r e314fb38307d src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Wed Dec 21 12:05:47 2005 +0100
+++ b/src/HOL/ROOT.ML	Wed Dec 21 12:06:08 2005 +0100
@@ -11,7 +11,6 @@
 
 use "hologic.ML";
 
-use "~~/src/Pure/General/hashtable.ML";
 use "~~/src/Provers/splitter.ML";
 use "~~/src/Provers/hypsubst.ML";
 use "~~/src/Provers/induct_method.ML";