# HG changeset patch
# User nipkow@lapbroy100.local
# Date 1232283195 -3600
# Node ID 02a52ae34b7a097a74a13ed570d6b3a2878b132b
# Parent  70ef35ccdc3b0b1e458e114f800a9d1570fc7cd4
bug fixes

diff -r 70ef35ccdc3b -r 02a52ae34b7a src/HOL/Tools/lin_arith.ML
--- 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
diff -r 70ef35ccdc3b -r 02a52ae34b7a src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Sat Jan 17 12:38:50 2009 +0100
+++ b/src/Provers/splitter.ML	Sun Jan 18 13:53:15 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)