1.1 --- a/src/HOL/Library/Numeral_Type.thy	Thu Feb 25 22:08:43 2010 +0100
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Thu Feb 25 22:15:27 2010 +0100
     1.3 @@ -167,7 +167,7 @@
     1.4  begin
     1.5  
     1.6  lemma size0: "0 < n"
     1.7 -by (cut_tac size1, simp)
     1.8 +using size1 by simp
     1.9  
    1.10  lemmas definitions =
    1.11    zero_def one_def add_def mult_def minus_def diff_def
    1.12 @@ -384,23 +384,18 @@
    1.13    "_NumeralType1" :: type ("1")
    1.14  
    1.15  translations
    1.16 -  "_NumeralType1" == (type) "num1"
    1.17 -  "_NumeralType0" == (type) "num0"
    1.18 +  (type) "1" == (type) "num1"
    1.19 +  (type) "0" == (type) "num0"
    1.20  
    1.21  parse_translation {*
    1.22  let
    1.23 -(* FIXME @{type_syntax} *)
    1.24 -val num1_const = Syntax.const "Numeral_Type.num1";
    1.25 -val num0_const = Syntax.const "Numeral_Type.num0";
    1.26 -val B0_const = Syntax.const "Numeral_Type.bit0";
    1.27 -val B1_const = Syntax.const "Numeral_Type.bit1";
    1.28 -
    1.29  fun mk_bintype n =
    1.30    let
    1.31 -    fun mk_bit n = if n = 0 then B0_const else B1_const;
    1.32 +    fun mk_bit 0 = Syntax.const @{type_syntax bit0}
    1.33 +      | mk_bit 1 = Syntax.const @{type_syntax bit1};
    1.34      fun bin_of n =
    1.35 -      if n = 1 then num1_const
    1.36 -      else if n = 0 then num0_const
    1.37 +      if n = 1 then Syntax.const @{type_syntax num1}
    1.38 +      else if n = 0 then Syntax.const @{type_syntax num0}
    1.39        else if n = ~1 then raise TERM ("negative type numeral", [])
    1.40        else
    1.41          let val (q, r) = Integer.div_mod n 2;
    1.42 @@ -419,25 +414,22 @@
    1.43  fun int_of [] = 0
    1.44    | int_of (b :: bs) = b + 2 * int_of bs;
    1.45  
    1.46 -(* FIXME @{type_syntax} *)
    1.47 -fun bin_of (Const ("num0", _)) = []
    1.48 -  | bin_of (Const ("num1", _)) = [1]
    1.49 -  | bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs
    1.50 -  | bin_of (Const ("bit1", _) $ bs) = 1 :: bin_of bs
    1.51 -  | bin_of t = raise TERM("bin_of", [t]);
    1.52 +fun bin_of (Const (@{type_syntax num0}, _)) = []
    1.53 +  | bin_of (Const (@{type_syntax num1}, _)) = [1]
    1.54 +  | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs
    1.55 +  | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs
    1.56 +  | bin_of t = raise TERM ("bin_of", [t]);
    1.57  
    1.58  fun bit_tr' b [t] =
    1.59 -  let
    1.60 -    val rev_digs = b :: bin_of t handle TERM _ => raise Match
    1.61 -    val i = int_of rev_digs;
    1.62 -    val num = string_of_int (abs i);
    1.63 -  in
    1.64 -    Syntax.const "_NumeralType" $ Syntax.free num
    1.65 -  end
    1.66 +      let
    1.67 +        val rev_digs = b :: bin_of t handle TERM _ => raise Match
    1.68 +        val i = int_of rev_digs;
    1.69 +        val num = string_of_int (abs i);
    1.70 +      in
    1.71 +        Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
    1.72 +      end
    1.73    | bit_tr' b _ = raise Match;
    1.74 -
    1.75 -(* FIXME @{type_syntax} *)
    1.76 -in [("bit0", bit_tr' 0), ("bit1", bit_tr' 1)] end;
    1.77 +in [(@{type_syntax bit0}, bit_tr' 0), (@{type_syntax bit1}, bit_tr' 1)] end;
    1.78  *}
    1.79  
    1.80  subsection {* Examples *}