src/HOL/Library/Numeral_Type.thy
changeset 35115 446c5063e4fd
parent 33361 1f18de40b43f
child 35362 828a42fb7445
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Thu Feb 11 22:55:16 2010 +0100
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Thu Feb 11 23:00:22 2010 +0100
     1.3 @@ -36,8 +36,8 @@
     1.4  
     1.5  typed_print_translation {*
     1.6  let
     1.7 -  fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_,[T,_]))] =
     1.8 -    Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T;
     1.9 +  fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_, [T, _]))] =
    1.10 +    Syntax.const @{syntax_const "_type_card"} $ Syntax.term_of_typ show_sorts T;
    1.11  in [(@{const_syntax card}, card_univ_tr')]
    1.12  end
    1.13  *}
    1.14 @@ -389,7 +389,7 @@
    1.15  
    1.16  parse_translation {*
    1.17  let
    1.18 -
    1.19 +(* FIXME @{type_syntax} *)
    1.20  val num1_const = Syntax.const "Numeral_Type.num1";
    1.21  val num0_const = Syntax.const "Numeral_Type.num0";
    1.22  val B0_const = Syntax.const "Numeral_Type.bit0";
    1.23 @@ -411,7 +411,7 @@
    1.24        mk_bintype (the (Int.fromString str))
    1.25    | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
    1.26  
    1.27 -in [("_NumeralType", numeral_tr)] end;
    1.28 +in [(@{syntax_const "_NumeralType"}, numeral_tr)] end;
    1.29  *}
    1.30  
    1.31  print_translation {*
    1.32 @@ -419,6 +419,7 @@
    1.33  fun int_of [] = 0
    1.34    | int_of (b :: bs) = b + 2 * int_of bs;
    1.35  
    1.36 +(* FIXME @{type_syntax} *)
    1.37  fun bin_of (Const ("num0", _)) = []
    1.38    | bin_of (Const ("num1", _)) = [1]
    1.39    | bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs
    1.40 @@ -435,6 +436,7 @@
    1.41    end
    1.42    | bit_tr' b _ = raise Match;
    1.43  
    1.44 +(* FIXME @{type_syntax} *)
    1.45  in [("bit0", bit_tr' 0), ("bit1", bit_tr' 1)] end;
    1.46  *}
    1.47