Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Datatype/datatype.ML
changeset 36692 54b64d4ad524
parent 36148 4ddcc2b07891
child 36945 9bec62c10714 
--- a/src/HOL/Tools/Datatype/datatype.ML	Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Wed May 05 18:25:34 2010 +0200
@@ -309,7 +309,7 @@
             val T' = typ_of_dtyp descr' sorts dt;
             val (Us, U) = strip_type T'
           in (case strip_dtyp dt of
-              (_, DtRec j) => if j mem ks' then
+              (_, DtRec j) => if member (op =) ks' j then
                   (i2 + 1, i2' + 1, ts @ [mk_lim (app_bnds
                      (mk_Free "y" (Us ---> Univ_elT) i2') (length Us)) Us],
                    Ts @ [Us ---> Univ_elT])
isabelle