diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/numeral_syntax.ML	Thu Jan 19 21:22:08 2006 +0100
@@ -8,7 +8,7 @@
 
 signature NUMERAL_SYNTAX =
 sig
-  val setup: (theory -> theory) list
+  val setup: theory -> theory
 end;
 
 structure NumeralSyntax: NUMERAL_SYNTAX =
@@ -55,9 +55,9 @@
 (* theory setup *)
 
 val setup =
- [Theory.hide_consts_i false ["Numeral.Pls", "Numeral.Min"],
-  Theory.hide_consts_i false ["Numeral.bit.B0", "Numeral.bit.B1"],
-   Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
-  Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
+  Theory.hide_consts_i false ["Numeral.Pls", "Numeral.Min"] #>
+  Theory.hide_consts_i false ["Numeral.bit.B0", "Numeral.bit.B1"] #>
+  Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
+  Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')];
 
 end;