src/HOL/Tools/sat_solver.ML

     (conjunction
     o (map disjunction)
     o (map (map literal_from_int))
     o clauses
     o (map int_from_string)
-    o (maps (String.tokens (fn c => c mem [#" ", #"\t", #"\n"])))
+    o (maps (String.tokens (member (op =) [#" ", #"\t", #"\n"])))
     o filter_preamble
     o filter (fn l => l <> "")
     o split_lines
     o File.read)
       path

       else
         (* set the lowest bit that wasn't set before, keep the higher bits *)
         SOME (y::x::xs)
     (* int list -> int -> bool *)
     fun assignment_from_list xs i =
-      i mem xs
+      member (op =) xs i
     (* int list -> SatSolver.result *)
     fun solver_loop xs =
       if PropLogic.eval (assignment_from_list xs) fm then
         SatSolver.SATISFIABLE (SOME o (assignment_from_list xs))
       else

           eval_and_force (xs@xs') fm'  (* xs and xs' should be distinct, so '@' here should have *)
                                        (* the same effect as 'union_int'                         *)
       end
       (* int list -> int option *)
       fun fresh_var xs =
-        Library.find_first (fn i => not (i mem_int xs) andalso not ((~i) mem_int xs)) indices
+        find_first (fn i => not (member (op =) xs i) andalso not (member (op =) xs (~i))) indices
       (* int list -> prop_formula -> int list option *)
       (* partial assignment 'xs' *)
       fun dpll xs fm =
       let
         val (xs', fm') = eval_and_force xs fm