src/HOL/Tools/Datatype/datatype.ML
changeset 36692 54b64d4ad524
parent 36148 4ddcc2b07891
child 36945 9bec62c10714
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -309,7 +309,7 @@
     1.4              val T' = typ_of_dtyp descr' sorts dt;
     1.5              val (Us, U) = strip_type T'
     1.6            in (case strip_dtyp dt of
     1.7 -              (_, DtRec j) => if j mem ks' then
     1.8 +              (_, DtRec j) => if member (op =) ks' j then
     1.9                    (i2 + 1, i2' + 1, ts @ [mk_lim (app_bnds
    1.10                       (mk_Free "y" (Us ---> Univ_elT) i2') (length Us)) Us],
    1.11                     Ts @ [Us ---> Univ_elT])