src/HOL/Tools/int_arith.ML
changeset 32603 e08fdd615333
parent 31510 e0f2bb4b0021
child 33296 a3924d1069e5
     1.1 --- a/src/HOL/Tools/int_arith.ML	Fri Sep 18 09:07:49 2009 +0200
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Fri Sep 18 09:07:50 2009 +0200
     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 HOL.one}, @{typ int})) = false
    1.10 +  | check (Const (@{const_name HOL.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 HOL.times}, @{const_name HOL.uminus},
    1.17 +      @{const_name HOL.minus}, @{const_name HOL.plus},
    1.18 +      @{const_name HOL.zero},
    1.19 +      @{const_name HOL.less}, @{const_name HOL.less_eq}] s
    1.20    | check (a $ b) = check a andalso check b
    1.21    | check _ = false;
    1.22