--- a/src/HOL/Integ/cooper_dec.ML Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Integ/cooper_dec.ML Tue Sep 20 16:17:34 2005 +0200
@@ -467,12 +467,12 @@
else HOLogic.false_const)
handle _ => at)
else
- case assoc (operations,p) of
+ case AList.lookup (op =) operations p of
SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)
handle _ => at)
| _ => at)
|Const("Not",_)$(Const (p,_) $ s $ t) =>(
- case assoc (operations,p) of
+ case AList.lookup (op =) operations p of
SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then
HOLogic.false_const else HOLogic.true_const)
handle _ => at)