src/HOL/Tools/sat_solver.ML
changeset 17494 e70600834f44
parent 17493 cf8713d880b1
child 17527 5c25f27da4ca
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Mon Sep 19 23:45:59 2005 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Tue Sep 20 00:16:29 2005 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4  (*      contains the IDs of clauses that must be resolved (in the given      *)
     1.5  (*      order) to obtain the new clause 'x'.  Each list 'xs' must be         *)
     1.6  (*      non-empty, and the literal to be resolved upon must always be unique *)
     1.7 -(*      (e.g. "A | ~B" must not be resolved with "~A| B").  Circular         *)
     1.8 +(*      (e.g. "A | ~B" must not be resolved with "~A | B").  Circular        *)
     1.9  (*      dependencies of clauses are not allowed.  (At least) one of the      *)
    1.10  (*      clauses in the table must be the empty clause (i.e. contain no       *)
    1.11  (*      literals); its ID is given by the second component of the proof.     *)
    1.12 @@ -591,7 +591,7 @@
    1.13  							val rs  = map int_from_string ids
    1.14  						in
    1.15  							(* update clause table *)
    1.16 -							(Inttab.update_new ((cid, rs), clause_table), conflict_id)
    1.17 +							(Inttab.update_new (cid, rs) clause_table, conflict_id)
    1.18  								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.")
    1.19  						end
    1.20  					| _ =>
    1.21 @@ -628,7 +628,7 @@
    1.22  							val rs   = aid :: map (fn v => !clause_offset + v) vids
    1.23  						in
    1.24  							(* update clause table *)
    1.25 -							(Inttab.update_new ((cid, rs), clause_table), conflict_id)
    1.26 +							(Inttab.update_new (cid, rs) clause_table, conflict_id)
    1.27  								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (antecedent for variable " ^ id ^ ") defined more than once.")
    1.28  						end
    1.29  					| _ =>