src/HOL/Import/hol4rews.ML
changeset 36692 54b64d4ad524
parent 35250 92664dca6f20
child 38551 8ddfc68a3908
     1.1 --- a/src/HOL/Import/hol4rews.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -604,9 +604,9 @@
     1.4                  val defname = Thm.def_name name
     1.5                  val pdefname = name ^ "_primdef"
     1.6              in
     1.7 -                if not (defname mem used)
     1.8 +                if not (member (op =) used defname)
     1.9                  then F defname                 (* name_def *)
    1.10 -                else if not (pdefname mem used)
    1.11 +                else if not (member (op =) used pdefname)
    1.12                  then F pdefname                (* name_primdef *)
    1.13                  else F (Name.variant used pdefname) (* last resort *)
    1.14              end