src/HOL/eqrule_HOL_data.ML
changeset 17521 0f1c48de39f5
parent 16587 b34c8aa657a5
child 18591 04b9f2bf5a48
     1.1 --- a/src/HOL/eqrule_HOL_data.ML	Tue Sep 20 15:12:40 2005 +0200
     1.2 +++ b/src/HOL/eqrule_HOL_data.ML	Tue Sep 20 16:17:34 2005 +0200
     1.3 @@ -45,8 +45,8 @@
     1.4             Const("Trueprop",_) $ p =>
     1.5               (case Term.head_of p of
     1.6                  Const(a,_) =>
     1.7 -                  (case Library.assoc(pairs,a) of
     1.8 -                     SOME(rls) => List.concat (map atoms ([th] RL rls))
     1.9 +                  (case AList.lookup (op =) pairs a of
    1.10 +                     SOME rls => List.concat (map atoms ([th] RL rls))
    1.11                     | NONE => [th])
    1.12                | _ => [th])
    1.13           | _ => [th])