1.1 --- a/src/HOL/Library/Numeral_Type.thy	Mon Jan 16 20:32:33 2012 +0100
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Mon Jan 16 21:50:15 2012 +0100
     1.3 @@ -296,7 +296,7 @@
     1.4  subsection {* Syntax *}
     1.5  
     1.6  syntax
     1.7 -  "_NumeralType" :: "num_const => type"  ("_")
     1.8 +  "_NumeralType" :: "num_token => type"  ("_")
     1.9    "_NumeralType0" :: type ("0")
    1.10    "_NumeralType1" :: type ("1")
    1.11  
    1.12 @@ -306,46 +306,45 @@
    1.13  
    1.14  parse_translation {*
    1.15  let
    1.16 -fun mk_bintype n =
    1.17 -  let
    1.18 -    fun mk_bit 0 = Syntax.const @{type_syntax bit0}
    1.19 -      | mk_bit 1 = Syntax.const @{type_syntax bit1};
    1.20 -    fun bin_of n =
    1.21 -      if n = 1 then Syntax.const @{type_syntax num1}
    1.22 -      else if n = 0 then Syntax.const @{type_syntax num0}
    1.23 -      else if n = ~1 then raise TERM ("negative type numeral", [])
    1.24 -      else
    1.25 -        let val (q, r) = Integer.div_mod n 2;
    1.26 -        in mk_bit r $ bin_of q end;
    1.27 -  in bin_of n end;
    1.28 +  fun mk_bintype n =
    1.29 +    let
    1.30 +      fun mk_bit 0 = Syntax.const @{type_syntax bit0}
    1.31 +        | mk_bit 1 = Syntax.const @{type_syntax bit1};
    1.32 +      fun bin_of n =
    1.33 +        if n = 1 then Syntax.const @{type_syntax num1}
    1.34 +        else if n = 0 then Syntax.const @{type_syntax num0}
    1.35 +        else if n = ~1 then raise TERM ("negative type numeral", [])
    1.36 +        else
    1.37 +          let val (q, r) = Integer.div_mod n 2;
    1.38 +          in mk_bit r $ bin_of q end;
    1.39 +    in bin_of n end;
    1.40  
    1.41 -fun numeral_tr (*"_NumeralType"*) [Const (str, _)] =
    1.42 -      mk_bintype (the (Int.fromString str))
    1.43 -  | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
    1.44 +  fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str))
    1.45 +    | numeral_tr ts = raise TERM ("numeral_tr", ts);
    1.46  
    1.47  in [(@{syntax_const "_NumeralType"}, numeral_tr)] end;
    1.48  *}
    1.49  
    1.50  print_translation {*
    1.51  let
    1.52 -fun int_of [] = 0
    1.53 -  | int_of (b :: bs) = b + 2 * int_of bs;
    1.54 +  fun int_of [] = 0
    1.55 +    | int_of (b :: bs) = b + 2 * int_of bs;
    1.56  
    1.57 -fun bin_of (Const (@{type_syntax num0}, _)) = []
    1.58 -  | bin_of (Const (@{type_syntax num1}, _)) = [1]
    1.59 -  | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs
    1.60 -  | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs
    1.61 -  | bin_of t = raise TERM ("bin_of", [t]);
    1.62 +  fun bin_of (Const (@{type_syntax num0}, _)) = []
    1.63 +    | bin_of (Const (@{type_syntax num1}, _)) = [1]
    1.64 +    | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs
    1.65 +    | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs
    1.66 +    | bin_of t = raise TERM ("bin_of", [t]);
    1.67  
    1.68 -fun bit_tr' b [t] =
    1.69 -      let
    1.70 -        val rev_digs = b :: bin_of t handle TERM _ => raise Match
    1.71 -        val i = int_of rev_digs;
    1.72 -        val num = string_of_int (abs i);
    1.73 -      in
    1.74 -        Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
    1.75 -      end
    1.76 -  | bit_tr' b _ = raise Match;
    1.77 +  fun bit_tr' b [t] =
    1.78 +        let
    1.79 +          val rev_digs = b :: bin_of t handle TERM _ => raise Match
    1.80 +          val i = int_of rev_digs;
    1.81 +          val num = string_of_int (abs i);
    1.82 +        in
    1.83 +          Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
    1.84 +        end
    1.85 +    | bit_tr' b _ = raise Match;
    1.86  in [(@{type_syntax bit0}, bit_tr' 0), (@{type_syntax bit1}, bit_tr' 1)] end;
    1.87  *}
    1.88