src/HOL/eqrule_HOL_data.ML

   let fun atoms th =
         (case Thm.concl_of th of
            Const("Trueprop",_) $ p =>
              (case Term.head_of p of
                 Const(a,_) =>
-                  (case Library.assoc(pairs,a) of
-                     SOME(rls) => List.concat (map atoms ([th] RL rls))
+                  (case AList.lookup (op =) pairs a of
+                     SOME rls => List.concat (map atoms ([th] RL rls))
                    | NONE => [th])
               | _ => [th])
          | _ => [th])
   in atoms end;