src/HOL/Tools/numeral_syntax.ML
changeset 13495 af27202d6d1c
parent 13491 ddf6ae639f21
child 14981 e73f8140af78
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Tue Aug 13 11:03:11 2002 +0200
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Tue Aug 13 12:16:14 2002 +0200
     1.3 @@ -30,11 +30,8 @@
     1.4        if pred x then 1 + prefix_len pred xs else 0;
     1.5  
     1.6  fun bin_of (Const ("bin.Pls", _)) = []
     1.7 -  | bin_of (Const ("Numeral.bin.Pls", _)) = []
     1.8    | bin_of (Const ("bin.Min", _)) = [~1]
     1.9 -  | bin_of (Const ("Numeral.bin.Min", _)) = [~1]
    1.10 -  | bin_of (Const ("bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    1.11 -  | bin_of (Const ("Numeral.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    1.12 +  | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    1.13    | bin_of _ = raise Match;
    1.14  
    1.15  val dest_bin = HOLogic.int_of o bin_of;
    1.16 @@ -74,9 +71,8 @@
    1.17  (* theory setup *)
    1.18  
    1.19  val setup =
    1.20 - [Theory.hide_consts false
    1.21 -    ["Numeral.bin.Pls", "Numeral.bin.Min"],
    1.22 -Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
    1.23 + [Theory.hide_consts false ["Numeral.bin.Pls", "Numeral.bin.Min"],
    1.24 +  Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
    1.25    Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
    1.26  
    1.27