src/HOL/Tools/Datatype/datatype_aux.ML
changeset 36692 54b64d4ad524
parent 35364 b8c62d60195c
child 38795 848be46708dc
     1.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -136,7 +136,7 @@
     1.4      val getP = if can HOLogic.dest_imp (hd ts) then
     1.5        (apfst SOME) o HOLogic.dest_imp else pair NONE;
     1.6      val flt = if null indnames then I else
     1.7 -      filter (fn Free (s, _) => s mem indnames | _ => false);
     1.8 +      filter (fn Free (s, _) => member (op =) indnames s | _ => false);
     1.9      fun abstr (t1, t2) = (case t1 of
    1.10          NONE => (case flt (OldTerm.term_frees t2) of
    1.11              [Free (s, T)] => SOME (absfree (s, T, t2))
    1.12 @@ -300,7 +300,7 @@
    1.13      fun is_nonempty_dt is i =
    1.14        let
    1.15          val (_, _, constrs) = (the o AList.lookup (op =) descr') i;
    1.16 -        fun arg_nonempty (_, DtRec i) = if i mem is then false
    1.17 +        fun arg_nonempty (_, DtRec i) = if member (op =) is i then false
    1.18                else is_nonempty_dt (i::is) i
    1.19            | arg_nonempty _ = true;
    1.20        in exists ((forall (arg_nonempty o strip_dtyp)) o snd) constrs