src/HOL/Integ/cooper_dec.ML
changeset 17521 0f1c48de39f5
parent 17485 c39871c52977
child 19233 77ca20b0ed77
     1.1 --- a/src/HOL/Integ/cooper_dec.ML	Tue Sep 20 15:12:40 2005 +0200
     1.2 +++ b/src/HOL/Integ/cooper_dec.ML	Tue Sep 20 16:17:34 2005 +0200
     1.3 @@ -467,12 +467,12 @@
     1.4       else HOLogic.false_const)
     1.5        handle _ => at)
     1.6      else
     1.7 -  case assoc (operations,p) of 
     1.8 +  case AList.lookup (op =) operations p of 
     1.9      SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
    1.10      handle _ => at) 
    1.11        | _ =>  at) 
    1.12        |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
    1.13 -  case assoc (operations,p) of 
    1.14 +  case AList.lookup (op =) operations p of 
    1.15      SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
    1.16      HOLogic.false_const else HOLogic.true_const)  
    1.17      handle _ => at)