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