--- a/src/HOL/Tools/lin_arith.ML Sat Jan 17 12:38:50 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML Sun Jan 18 13:53:15 2009 +0100
@@ -149,9 +149,9 @@
fun add_atom (t : term) (m : Rat.rat) (p : (term * Rat.rat) list, i : Rat.rat) :
(term * Rat.rat) list * Rat.rat =
- case AList.lookup (op =) p t of
+ case AList.lookup Pattern.aeconv p t of
NONE => ((t, m) :: p, i)
- | SOME n => (AList.update (op =) (t, Rat.add n m) p, i);
+ | SOME n => (AList.update Pattern.aeconv (t, Rat.add n m) p, i);
(* decompose nested multiplications, bracketing them to the right and combining
all their coefficients