--- 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;