diff -r 0a5eebd5ff58 -r d9d50222808e src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Mon Sep 12 17:29:07 2005 +0200
+++ b/src/FOL/simpdata.ML	Mon Sep 12 18:20:32 2005 +0200
@@ -115,7 +115,7 @@
            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])