avoid some garbage
authorschirmer
Tue Jul 12 23:42:11 2005 +0200 (2005-07-12)
changeset 1678326fccaaf9cb4
parent 16782 b214f21ae396
child 16784 92ff7c903585
avoid some garbage
src/HOL/Tools/record_package.ML
     1.1 --- a/src/HOL/Tools/record_package.ML	Tue Jul 12 21:49:38 2005 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Tue Jul 12 23:42:11 2005 +0200
     1.3 @@ -859,6 +859,7 @@
     1.4  fun get_fields extfields T = 
     1.5       Library.foldl (fn (xs,(eN,_))=>xs@(Symtab.lookup_multi (extfields,eN)))
     1.6               ([],(dest_recTs T));
     1.7 +fun eq s1 s2 = (String.compare (s1, s2) = EQUAL);
     1.8  in
     1.9  (* record_simproc *)
    1.10  (* Simplifies selections of an record update:
    1.11 @@ -893,8 +894,8 @@
    1.12                                 val kv = mk_abs_var "k" k
    1.13                                 val kb = Bound 1 
    1.14                               in SOME (upd$kb$rb,kb,[kv,rv],true) end
    1.15 -                        else if u_name mem (map fst (get_fields extfields rangeS))
    1.16 -                             orelse s mem (map fst (get_fields extfields updT))
    1.17 +                        else if exists (eq u_name o fst) (get_fields extfields rangeS)
    1.18 +                             orelse exists (eq s o fst) (get_fields extfields updT)
    1.19                               then NONE
    1.20  			     else (case mk_eq_terms r of 
    1.21                                       SOME (trm,trm',vars,update_s) 
    1.22 @@ -944,7 +945,7 @@
    1.23               fun sel_name u = NameSpace.base (unsuffix updateN u);
    1.24  
    1.25               fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) =
    1.26 -                  if s mem (map fst (get_fields extfields mT)) then upd else seed s r
    1.27 +                  if exists (eq s o fst) (get_fields extfields mT) then upd else seed s r
    1.28                 | seed _ r = r;
    1.29  
    1.30               fun grow u uT k vars (sprout,skeleton) =