src/HOL/Tools/Presburger/cooper_proof.ML

 (* Finding rho and beta for evalc *)
 (* -------------------------------*)
 
 fun rho_for_evalc sg at = case at of  
     (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 prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)) 
              else prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const)))  
 		   handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl)
         | _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl )
      |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 prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))  
              else prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)))  
 		      handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl)