src/HOL/Tools/numeral_syntax.ML
changeset 35115 446c5063e4fd
parent 29316 0a7fcdd77f4b
child 35123 e286d5df187a
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Thu Feb 11 22:55:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Thu Feb 11 23:00:22 2010 +0100
     1.3 @@ -27,7 +27,7 @@
     1.4  in
     1.5  
     1.6  fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] =
     1.7 -      Syntax.const @{const_name Int.number_of} $ mk_bin num
     1.8 +      Syntax.const @{const_syntax Int.number_of} $ mk_bin num
     1.9    | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    1.10  
    1.11  end;
    1.12 @@ -37,10 +37,10 @@
    1.13  
    1.14  local
    1.15  
    1.16 -fun dest_bin (Const (@{const_syntax "Int.Pls"}, _)) = []
    1.17 -  | dest_bin (Const (@{const_syntax "Int.Min"}, _)) = [~1]
    1.18 -  | dest_bin (Const (@{const_syntax "Int.Bit0"}, _) $ bs) = 0 :: dest_bin bs
    1.19 -  | dest_bin (Const (@{const_syntax "Int.Bit1"}, _) $ bs) = 1 :: dest_bin bs
    1.20 +fun dest_bin (Const (@{const_syntax Int.Pls}, _)) = []
    1.21 +  | dest_bin (Const (@{const_syntax Int.Min}, _)) = [~1]
    1.22 +  | dest_bin (Const (@{const_syntax Int.Bit0}, _) $ bs) = 0 :: dest_bin bs
    1.23 +  | dest_bin (Const (@{const_syntax Int.Bit1}, _) $ bs) = 1 :: dest_bin bs
    1.24    | dest_bin _ = raise Match;
    1.25  
    1.26  fun leading _ [] = 0
    1.27 @@ -64,11 +64,12 @@
    1.28    end;
    1.29  
    1.30  fun syntax_numeral t =
    1.31 -  Syntax.const "_Numeral" $ (Syntax.const "_numeral" $ Syntax.free (dest_bin_str t));
    1.32 +  Syntax.const @{syntax_const "_Numeral"} $
    1.33 +    (Syntax.const @{syntax_const "_numeral"} $ Syntax.free (dest_bin_str t));
    1.34  
    1.35  in
    1.36  
    1.37 -fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
    1.38 +fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =  (* FIXME @{type_syntax} *)
    1.39        let val t' =
    1.40          if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t
    1.41          else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
    1.42 @@ -84,7 +85,7 @@
    1.43  (* theory setup *)
    1.44  
    1.45  val setup =
    1.46 -  Sign.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
    1.47 +  Sign.add_trfuns ([], [(@{syntax_const "_Numeral"}, numeral_tr)], [], []) #>
    1.48    Sign.add_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')];
    1.49  
    1.50  end;