src/HOL/Tools/numeral_syntax.ML
changeset 15013 34264f5e4691
parent 14981 e73f8140af78
child 15595 dc8a41c7cefc
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Wed Jun 30 14:04:58 2004 +0200
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Thu Jul 01 12:29:53 2004 +0200
     1.3 @@ -28,8 +28,8 @@
     1.4    | prefix_len pred (x :: xs) =
     1.5        if pred x then 1 + prefix_len pred xs else 0;
     1.6  
     1.7 -fun bin_of (Const ("bin.Pls", _)) = []
     1.8 -  | bin_of (Const ("bin.Min", _)) = [~1]
     1.9 +fun bin_of (Const ("Numeral.Pls", _)) = []
    1.10 +  | bin_of (Const ("Numeral.Min", _)) = [~1]
    1.11    | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    1.12    | bin_of _ = raise Match;
    1.13  
    1.14 @@ -70,7 +70,7 @@
    1.15  (* theory setup *)
    1.16  
    1.17  val setup =
    1.18 - [Theory.hide_consts false ["Numeral.bin.Pls", "Numeral.bin.Min"],
    1.19 + [Theory.hide_consts false ["Numeral.Pls", "Numeral.Min"],
    1.20    Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
    1.21    Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
    1.22