src/ZF/Tools/numeral_syntax.ML
changeset 18708 4b3dadb4fe33
parent 15965 f422f8283491
child 21781 8314ebb5364d
     1.1 --- a/src/ZF/Tools/numeral_syntax.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/ZF/Tools/numeral_syntax.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4    val mk_bin   : IntInf.int -> term
     1.5    val int_tr   : term list -> term
     1.6    val int_tr'  : bool -> typ -> term list -> term
     1.7 -  val setup    : (theory -> theory) list
     1.8 +  val setup    : theory -> theory
     1.9  end;
    1.10  
    1.11  structure NumeralSyntax: NUMERAL_SYNTAX =
    1.12 @@ -100,7 +100,7 @@
    1.13  
    1.14  
    1.15  val setup =
    1.16 - [Theory.add_trfuns ([], [("_Int", int_tr)], [], []),
    1.17 -  Theory.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]];
    1.18 + (Theory.add_trfuns ([], [("_Int", int_tr)], [], []) #>
    1.19 +  Theory.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]);
    1.20  
    1.21  end;