src/FOLP/simp.ML
changeset 17325 d9d50222808e
parent 16931 e41d8e319dfd
child 19805 854404b8f738
     1.1 --- a/src/FOLP/simp.ML	Mon Sep 12 17:29:07 2005 +0200
     1.2 +++ b/src/FOLP/simp.ML	Mon Sep 12 18:20:32 2005 +0200
     1.3 @@ -179,7 +179,7 @@
     1.4          fun add_vars (tm,vars) = case tm of
     1.5                    Abs (_,_,body) => add_vars(body,vars)
     1.6                  | r$s => (case head_of tm of
     1.7 -                          Const(c,T) => (case assoc(new_asms,c) of
     1.8 +                          Const(c,T) => (case AList.lookup (op =) new_asms c of
     1.9                                    NONE => add_vars(r,add_vars(s,vars))
    1.10                                  | SOME(al) => add_list(tm,al,vars))
    1.11                          | _ => add_vars(r,add_vars(s,vars)))