--- 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;