diff -r 46652582f831 -r 870a953e0a8c src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Tue Jul 06 21:09:05 1999 +0200
+++ b/src/HOL/ROOT.ML	Tue Jul 06 21:09:23 1999 +0200
@@ -52,6 +52,7 @@
 use "Tools/datatype_package.ML";
 use "Tools/primrec_package.ML";
 use_thy "Datatype";
+use_thy "Numeral";
 
 use "Tools/record_package.ML";
 use_thy "Record";