src/HOL/Tools/Quotient/quotient_term.ML
changeset 36692 54b64d4ad524
parent 35990 5ceedb86aa9d
child 37135 636e6d8645d6
     1.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -728,7 +728,7 @@
     1.4    val all_ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
     1.5    val ty_substs =
     1.6      if qtys = [] then all_ty_substs else
     1.7 -    filter (fn (_, qty) => qty mem qtys) all_ty_substs
     1.8 +    filter (fn (_, qty) => member (op =) qtys qty) all_ty_substs
     1.9    val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos
    1.10    fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel)))
    1.11    val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos