src/HOL/Library/reflection.ML
changeset 36692 54b64d4ad524
parent 35624 c4e29a0bb8c1
child 36945 9bec62c10714
     1.1 --- a/src/HOL/Library/reflection.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Library/reflection.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -149,7 +149,7 @@
     1.4                Pattern.match thy
     1.5                  ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
     1.6                  (Vartab.empty, Vartab.empty)
     1.7 -            val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv)
     1.8 +            val (fnvs,invs) = List.partition (fn ((vn,_),_) => member (op =) vns vn) (Vartab.dest tmenv)
     1.9              val (fts,its) =
    1.10                (map (snd o snd) fnvs,
    1.11                 map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)