src/ZF/Tools/numeral_syntax.ML
changeset 23146 0bc590051d95
parent 21781 8314ebb5364d
child 24630 351a308ab58d
--- a/src/ZF/Tools/numeral_syntax.ML	Thu May 31 11:00:06 2007 +0200
+++ b/src/ZF/Tools/numeral_syntax.ML	Thu May 31 12:06:31 2007 +0200
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
 Concrete syntax for generic numerals.  Assumes consts and syntax of
-theory ZF/Integ/Bin.
+theory Bin.
 *)
 
 signature NUMERAL_SYNTAX =