--- a/src/ZF/Tools/numeral_syntax.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/ZF/Tools/numeral_syntax.ML Thu Jan 19 21:22:08 2006 +0100
@@ -12,7 +12,7 @@
val mk_bin : IntInf.int -> term
val int_tr : term list -> term
val int_tr' : bool -> typ -> term list -> term
- val setup : (theory -> theory) list
+ val setup : theory -> theory
end;
structure NumeralSyntax: NUMERAL_SYNTAX =
@@ -100,7 +100,7 @@
val setup =
- [Theory.add_trfuns ([], [("_Int", int_tr)], [], []),
- Theory.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]];
+ (Theory.add_trfuns ([], [("_Int", int_tr)], [], []) #>
+ Theory.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]);
end;