# HG changeset patch
# User schirmer
# Date 1121204531 -7200
# Node ID 26fccaaf9cb458b344bac162b62dd6f6fa321b47
# Parent  b214f21ae396ec1ae1b724103ec1189440020acc
avoid some garbage

diff -r b214f21ae396 -r 26fccaaf9cb4 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue Jul 12 21:49:38 2005 +0200
+++ b/src/HOL/Tools/record_package.ML	Tue Jul 12 23:42:11 2005 +0200
@@ -859,6 +859,7 @@
 fun get_fields extfields T = 
      Library.foldl (fn (xs,(eN,_))=>xs@(Symtab.lookup_multi (extfields,eN)))
              ([],(dest_recTs T));
+fun eq s1 s2 = (String.compare (s1, s2) = EQUAL);
 in
 (* record_simproc *)
 (* Simplifies selections of an record update:
@@ -893,8 +894,8 @@
                                val kv = mk_abs_var "k" k
                                val kb = Bound 1 
                              in SOME (upd$kb$rb,kb,[kv,rv],true) end
-                        else if u_name mem (map fst (get_fields extfields rangeS))
-                             orelse s mem (map fst (get_fields extfields updT))
+                        else if exists (eq u_name o fst) (get_fields extfields rangeS)
+                             orelse exists (eq s o fst) (get_fields extfields updT)
                              then NONE
 			     else (case mk_eq_terms r of 
                                      SOME (trm,trm',vars,update_s) 
@@ -944,7 +945,7 @@
              fun sel_name u = NameSpace.base (unsuffix updateN u);
 
              fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) =
-                  if s mem (map fst (get_fields extfields mT)) then upd else seed s r
+                  if exists (eq s o fst) (get_fields extfields mT) then upd else seed s r
                | seed _ r = r;
 
              fun grow u uT k vars (sprout,skeleton) =