Theory.hide_consts renamed to Theory.hide_consts_i;
authorwenzelm
Sat Jun 11 22:15:50 2005 +0200 (2005-06-11)
changeset 16365838c65dad23a
parent 16364 dc9f7066d80a
child 16366 6ff17d08c3d5
Theory.hide_consts renamed to Theory.hide_consts_i;
src/HOL/Tools/numeral_syntax.ML
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Sat Jun 11 22:15:48 2005 +0200
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Sat Jun 11 22:15:50 2005 +0200
     1.3 @@ -55,8 +55,8 @@
     1.4  (* theory setup *)
     1.5  
     1.6  val setup =
     1.7 - [Theory.hide_consts false ["Numeral.Pls", "Numeral.Min"],
     1.8 -  Theory.hide_consts false ["Numeral.bit.B0", "Numeral.bit.B1"],
     1.9 + [Theory.hide_consts_i false ["Numeral.Pls", "Numeral.Min"],
    1.10 +  Theory.hide_consts_i false ["Numeral.bit.B0", "Numeral.bit.B1"],
    1.11     Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
    1.12    Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
    1.13