src/FOL/simpdata.ML

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