src/HOL/simpdata.ML
changeset 17325 d9d50222808e
parent 17197 917c6e7ca28d
child 17778 93d7e524417a
     1.1 --- a/src/HOL/simpdata.ML	Mon Sep 12 17:29:07 2005 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Mon Sep 12 18:20:32 2005 +0200
     1.3 @@ -285,7 +285,7 @@
     1.4             Const("Trueprop",_) $ p =>
     1.5               (case head_of p 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 atoms ([th] RL rls))
    1.10                     | NONE => [th])
    1.11                | _ => [th])