src/HOL/Tools/lin_arith.ML
changeset 36692 54b64d4ad524
parent 36001 992839c4be90
child 37388 793618618f78
     1.1 --- a/src/HOL/Tools/lin_arith.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/lin_arith.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -221,7 +221,7 @@
     1.4          in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k2))) end
     1.5          handle TERM _ => add_atom all m pi)
     1.6      | poly (all as Const f $ x, m, pi) =
     1.7 -        if f mem inj_consts then poly (x, m, pi) else add_atom all m pi
     1.8 +        if member (op =) inj_consts f then poly (x, m, pi) else add_atom all m pi
     1.9      | poly (all, m, pi) =
    1.10          add_atom all m pi
    1.11    val (p, i) = poly (lhs, Rat.one, ([], Rat.zero))