1.1 --- a/src/HOL/Import/proof_kernel.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -276,6 +276,7 @@
     1.4      in
     1.5          F
     1.6      end
     1.7 +infix mem;
     1.8  fun i mem L =
     1.9      let fun itr [] = false
    1.10            | itr (a::rst) = i=a orelse itr rst
    1.11 @@ -1091,7 +1092,7 @@
    1.12      let
    1.13          fun F vars (Bound _) = vars
    1.14            | F vars (tm as Free _) =
    1.15 -            if tm mem vars
    1.16 +            if member (op =) vars tm
    1.17              then vars
    1.18              else (tm::vars)
    1.19            | F vars (Const _) = vars