diff -r 102a0a0718c5 -r eac4bb5adbf9 src/HOL/Tools/numeral.ML
--- a/src/HOL/Tools/numeral.ML	Thu Feb 28 16:38:17 2013 +0100
+++ b/src/HOL/Tools/numeral.ML	Thu Feb 28 16:54:52 2013 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Tools/numeral.ML
     Author:     Makarius
 
-Logical operations on numerals (see also HOL/hologic.ML).
+Logical operations on numerals (see also HOL/Tools/hologic.ML).
 *)
 
 signature NUMERAL =