src/HOL/Tools/int_arith.ML
changeset 38864 4abe644fcea5
parent 38763 283f1f9969ba
child 42795 66fcc9882784
     1.1 --- a/src/HOL/Tools/int_arith.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4  
     1.5  fun check (Const (@{const_name Groups.one}, @{typ int})) = false
     1.6    | check (Const (@{const_name Groups.one}, _)) = true
     1.7 -  | check (Const (s, _)) = member (op =) [@{const_name "op ="},
     1.8 +  | check (Const (s, _)) = member (op =) [@{const_name HOL.eq},
     1.9        @{const_name Groups.times}, @{const_name Groups.uminus},
    1.10        @{const_name Groups.minus}, @{const_name Groups.plus},
    1.11        @{const_name Groups.zero},