src/HOL/Tools/int_arith.ML
changeset 34974 18b41bba42b5
parent 33296 a3924d1069e5
child 35028 108662d50512
     1.1 --- a/src/HOL/Tools/int_arith.ML	Thu Jan 28 11:48:43 2010 +0100
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Thu Jan 28 11:48:49 2010 +0100
     1.3 @@ -49,13 +49,13 @@
     1.4    make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
     1.5    proc = proc1, identifier = []};
     1.6  
     1.7 -fun check (Const (@{const_name HOL.one}, @{typ int})) = false
     1.8 -  | check (Const (@{const_name HOL.one}, _)) = true
     1.9 +fun check (Const (@{const_name Algebras.one}, @{typ int})) = false
    1.10 +  | check (Const (@{const_name Algebras.one}, _)) = true
    1.11    | check (Const (s, _)) = member (op =) [@{const_name "op ="},
    1.12 -      @{const_name HOL.times}, @{const_name HOL.uminus},
    1.13 -      @{const_name HOL.minus}, @{const_name HOL.plus},
    1.14 -      @{const_name HOL.zero},
    1.15 -      @{const_name HOL.less}, @{const_name HOL.less_eq}] s
    1.16 +      @{const_name Algebras.times}, @{const_name Algebras.uminus},
    1.17 +      @{const_name Algebras.minus}, @{const_name Algebras.plus},
    1.18 +      @{const_name Algebras.zero},
    1.19 +      @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
    1.20    | check (a $ b) = check a andalso check b
    1.21    | check _ = false;
    1.22