diff -r ba1f6aba44ed -r 7fa91e6176ed src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Jul 13 20:07:01 2005 +0200
+++ b/src/HOL/Tools/record_package.ML	Wed Jul 13 20:53:26 2005 +0200
@@ -855,11 +855,10 @@
 
 
 local
-
-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);
+fun eq (s1:string) (s2:string) = (s1 = s2);
+fun has_field extfields f T =
+     exists (fn (eN,_) => exists (eq f o fst) (Symtab.lookup_multi (extfields,eN))) 
+       (dest_recTs T);
 in
 (* record_simproc *)
 (* Simplifies selections of an record update:
@@ -894,8 +893,8 @@
                                val kv = mk_abs_var "k" k
                                val kb = Bound 1 
                              in SOME (upd$kb$rb,kb,[kv,rv],true) end
-                        else if exists (eq u_name o fst) (get_fields extfields rangeS)
-                             orelse exists (eq s o fst) (get_fields extfields updT)
+                        else if has_field extfields u_name rangeS
+                             orelse has_field extfields s updT
                              then NONE
 			     else (case mk_eq_terms r of 
                                      SOME (trm,trm',vars,update_s) 
@@ -945,7 +944,7 @@
              fun sel_name u = NameSpace.base (unsuffix updateN u);
 
              fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) =
-                  if exists (eq s o fst) (get_fields extfields mT) then upd else seed s r
+                  if has_field extfields s mT then upd else seed s r
                | seed _ r = r;
 
              fun grow u uT k vars (sprout,skeleton) =