src/HOL/Tools/numeral_syntax.ML
changeset 11701 3d51fbf81c17
parent 11488 4ff900551340
child 13110 ca8cd110f769
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Fri Oct 05 21:50:37 2001 +0200
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Fri Oct 05 21:52:39 2001 +0200
     1.3 @@ -50,8 +50,12 @@
     1.4        (case rev rev_digs of
     1.5          ~1 :: bs => ("-", prefix_len (equal 1) bs)
     1.6        | bs => ("", prefix_len (equal 0) bs));
     1.7 -    val num = string_of_int (abs (HOLogic.int_of rev_digs));
     1.8 -  in "#" ^ sign ^ implode (replicate zs "0") ^ num end;
     1.9 +    val i = HOLogic.int_of rev_digs;
    1.10 +    val num = string_of_int (abs i);
    1.11 +  in
    1.12 +    if i = 0 orelse i = 1 then raise Match
    1.13 +    else sign ^ implode (replicate zs "0") ^ num
    1.14 +  end;
    1.15  
    1.16  
    1.17  (* translation of integer numeral tokens to and from bitstrings *)