diff -r e8bba7723858 -r 64ed05609568 src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML	Tue Sep 25 17:06:14 2007 +0200
@@ -88,7 +88,7 @@
 (* theory setup *)
 
 val setup =
-  Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
-  Theory.add_trfunsT [(@{const_syntax Numeral.number_of}, numeral_tr')];
+  Sign.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
+  Sign.add_trfunsT [(@{const_syntax Numeral.number_of}, numeral_tr')];
 
 end;