# HG changeset patch
# User wenzelm
# Date 1144601475 -7200
# Node ID 6cd8abc7f15b6a58f9ad27caf0f4ea6a70ab8e37
# Parent  b808efaa5828f6c33313efcc3a76377b9e8f5064
hide consts in Numeral.thy;

diff -r b808efaa5828 -r 6cd8abc7f15b src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Sun Apr 09 18:51:13 2006 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML	Sun Apr 09 18:51:15 2006 +0200
@@ -55,8 +55,6 @@
 (* theory setup *)
 
 val setup =
-  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')];