# HG changeset patch
# User wenzelm
# Date 1029233774 -7200
# Node ID af27202d6d1c4b0a791a59128a2300e67f1d524d
# Parent  1c44289716aeba91550fe6b05104534aac507fbd
more robust printing of numerals;

diff -r 1c44289716ae -r af27202d6d1c src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Tue Aug 13 11:03:11 2002 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML	Tue Aug 13 12:16:14 2002 +0200
@@ -30,11 +30,8 @@
       if pred x then 1 + prefix_len pred xs else 0;
 
 fun bin_of (Const ("bin.Pls", _)) = []
-  | bin_of (Const ("Numeral.bin.Pls", _)) = []
   | bin_of (Const ("bin.Min", _)) = [~1]
-  | bin_of (Const ("Numeral.bin.Min", _)) = [~1]
-  | bin_of (Const ("bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
-  | bin_of (Const ("Numeral.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
+  | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
   | bin_of _ = raise Match;
 
 val dest_bin = HOLogic.int_of o bin_of;
@@ -74,9 +71,8 @@
 (* theory setup *)
 
 val setup =
- [Theory.hide_consts false
-    ["Numeral.bin.Pls", "Numeral.bin.Min"],
-Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
+ [Theory.hide_consts false ["Numeral.bin.Pls", "Numeral.bin.Min"],
+  Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
   Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];