src/HOL/Tools/numeral_syntax.ML
changeset 18708 4b3dadb4fe33
parent 16365 838c65dad23a
child 19381 6cd8abc7f15b
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  signature NUMERAL_SYNTAX =
     1.6  sig
     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 @@ -55,9 +55,9 @@
    1.13  (* theory setup *)
    1.14  
    1.15  val setup =
    1.16 - [Theory.hide_consts_i false ["Numeral.Pls", "Numeral.Min"],
    1.17 -  Theory.hide_consts_i false ["Numeral.bit.B0", "Numeral.bit.B1"],
    1.18 -   Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
    1.19 -  Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
    1.20 +  Theory.hide_consts_i false ["Numeral.Pls", "Numeral.Min"] #>
    1.21 +  Theory.hide_consts_i false ["Numeral.bit.B0", "Numeral.bit.B1"] #>
    1.22 +  Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
    1.23 +  Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')];
    1.24  
    1.25  end;