src/ZF/Bin.thy

--- a/src/ZF/Bin.thy	Sat Mar 01 14:10:15 2008 +0100
+++ b/src/ZF/Bin.thy	Sat Mar 01 15:01:03 2008 +0100
@@ -18,7 +18,7 @@
 
 theory Bin
 imports Int_ZF Datatype_ZF
-uses "Tools/numeral_syntax.ML"
+uses ("Tools/numeral_syntax.ML")
 begin
 
 consts  bin :: i
@@ -27,6 +27,8 @@
         | Min
         | Bit ("w: bin", "b: bool")	(infixl "BIT" 90)
 
+use "Tools/numeral_syntax.ML"
+
 syntax
   "_Int"    :: "xnum => i"        ("_")