--- 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) =