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