src/Provers/Arith/fast_lin_arith.ML

      end handle FalseE thm => (trace_thm "False reached early:" thm; thm)
   end
 end;
 
 fun coeff poly atom : IntInf.int =
-  case assoc(poly,atom) of NONE => 0 | SOME i => i;
+  AList.lookup (op =) poly atom |> the_default 0;
 
 fun lcms is = Library.foldl lcm (1, is);
 
 fun integ(rlhs,r,rel,rrhs,s,d) =
 let val (rn,rd) = rep_rat r and (sn,sd) = rep_rat s