--- a/src/HOL/Tools/lin_arith.ML Sun Jan 18 10:11:12 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML Sun Jan 18 13:58:17 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
--- a/src/Provers/splitter.ML Sun Jan 18 10:11:12 2009 +0100
+++ b/src/Provers/splitter.ML Sun Jan 18 13:58:17 2009 +0100
@@ -146,7 +146,7 @@
fun mk_cntxt_splitthm t tt T =
let fun repl lev t =
- if incr_boundvars lev tt aconv t then Bound lev
+ if Pattern.aeconv(incr_boundvars lev tt, t) then Bound lev
else case t of
(Abs (v, T2, t)) => Abs (v, T2, repl (lev+1) t)
| (Bound i) => Bound (if i>=lev then i+1 else i)