src/HOL/Tools/sat_solver.ML
changeset 36692 54b64d4ad524
parent 35011 9e55e87434ff
child 37254 3625d37a0079
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -350,7 +350,7 @@
     1.4      o (map (map literal_from_int))
     1.5      o clauses
     1.6      o (map int_from_string)
     1.7 -    o (maps (String.tokens (fn c => c mem [#" ", #"\t", #"\n"])))
     1.8 +    o (maps (String.tokens (member (op =) [#" ", #"\t", #"\n"])))
     1.9      o filter_preamble
    1.10      o filter (fn l => l <> "")
    1.11      o split_lines
    1.12 @@ -421,7 +421,7 @@
    1.13          SOME (y::x::xs)
    1.14      (* int list -> int -> bool *)
    1.15      fun assignment_from_list xs i =
    1.16 -      i mem xs
    1.17 +      member (op =) xs i
    1.18      (* int list -> SatSolver.result *)
    1.19      fun solver_loop xs =
    1.20        if PropLogic.eval (assignment_from_list xs) fm then
    1.21 @@ -490,7 +490,7 @@
    1.22        end
    1.23        (* int list -> int option *)
    1.24        fun fresh_var xs =
    1.25 -        Library.find_first (fn i => not (i mem_int xs) andalso not ((~i) mem_int xs)) indices
    1.26 +        find_first (fn i => not (member (op =) xs i) andalso not (member (op =) xs (~i))) indices
    1.27        (* int list -> prop_formula -> int list option *)
    1.28        (* partial assignment 'xs' *)
    1.29        fun dpll xs fm =