src/ZF/simpdata.ML
changeset 17325 d9d50222808e
parent 17002 fb9261990ffe
child 17876 b9c92f384109
     1.1 --- a/src/ZF/simpdata.ML	Mon Sep 12 17:29:07 2005 +0200
     1.2 +++ b/src/ZF/simpdata.ML	Mon Sep 12 18:20:32 2005 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    let fun tryrules pairs t =
     1.5            case head_of t of
     1.6                Const(a,_) =>
     1.7 -                (case assoc(pairs,a) of
     1.8 +                (case AList.lookup (op =) pairs a of
     1.9                       SOME rls => List.concat (map (atomize (conn_pairs, mem_pairs))
    1.10                                         ([th] RL rls))
    1.11                     | NONE     => [th])