# HG changeset patch
# User wenzelm
# Date 1118520950 -7200
# Node ID 838c65dad23a17ede4488825c92ef2bddea170ea
# Parent  dc9f7066d80a76e7e68405e2904a3c8331650a8b
Theory.hide_consts renamed to Theory.hide_consts_i;

diff -r dc9f7066d80a -r 838c65dad23a src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Sat Jun 11 22:15:48 2005 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML	Sat Jun 11 22:15:50 2005 +0200
@@ -55,8 +55,8 @@
 (* theory setup *)
 
 val setup =
- [Theory.hide_consts false ["Numeral.Pls", "Numeral.Min"],
-  Theory.hide_consts false ["Numeral.bit.B0", "Numeral.bit.B1"],
+ [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')]];