# HG changeset patch
# User nipkow
# Date 1232192285 -3600
# Node ID 00fe02648e5dd3afee0c1aad0ae2a7aee736816e
# Parent  4dff3b11f64d72b08b21872ea30c68d099de9866
bug fix

diff -r 4dff3b11f64d -r 00fe02648e5d src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Fri Jan 16 16:00:20 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Sat Jan 17 12:38:05 2009 +0100
@@ -340,7 +340,7 @@
 
 fun subst_term ([] : (term * term) list) (t : term) = t
   | subst_term pairs                     t          =
-      (case AList.lookup (op aconv) pairs t of
+      (case AList.lookup Pattern.aeconv pairs t of
         SOME new =>
           new
       | NONE     =>
@@ -682,7 +682,7 @@
 
 fun negated_term_occurs_positively (terms : term list) : bool =
   List.exists
-    (fn (Trueprop $ (Const ("Not", _) $ t)) => member (op aconv) terms (Trueprop $ t)
+    (fn (Trueprop $ (Const ("Not", _) $ t)) => member Pattern.aeconv terms (Trueprop $ t)
       | _                                   => false)
     terms;