Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/FOL/simpdata.ML
changeset 17325 d9d50222808e
parent 17002 fb9261990ffe
child 17875 d81094515061 
--- 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])
isabelle