# HG changeset patch
# User webertj
# Date 1127168189 -7200
# Node ID e70600834f447d79ec7ac62ddef505ceca6f8fa6
# Parent  cf8713d880b1141e2e90ade9a283e6c15f4ac7ba
using curried Inttab.update_new function now

diff -r cf8713d880b1 -r e70600834f44 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Mon Sep 19 23:45:59 2005 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Tue Sep 20 00:16:29 2005 +0200
@@ -56,7 +56,7 @@
 (*      contains the IDs of clauses that must be resolved (in the given      *)
 (*      order) to obtain the new clause 'x'.  Each list 'xs' must be         *)
 (*      non-empty, and the literal to be resolved upon must always be unique *)
-(*      (e.g. "A | ~B" must not be resolved with "~A| B").  Circular         *)
+(*      (e.g. "A | ~B" must not be resolved with "~A | B").  Circular        *)
 (*      dependencies of clauses are not allowed.  (At least) one of the      *)
 (*      clauses in the table must be the empty clause (i.e. contain no       *)
 (*      literals); its ID is given by the second component of the proof.     *)
@@ -591,7 +591,7 @@
 							val rs  = map int_from_string ids
 						in
 							(* update clause table *)
-							(Inttab.update_new ((cid, rs), clause_table), conflict_id)
+							(Inttab.update_new (cid, rs) clause_table, conflict_id)
 								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.")
 						end
 					| _ =>
@@ -628,7 +628,7 @@
 							val rs   = aid :: map (fn v => !clause_offset + v) vids
 						in
 							(* update clause table *)
-							(Inttab.update_new ((cid, rs), clause_table), conflict_id)
+							(Inttab.update_new (cid, rs) clause_table, conflict_id)
 								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (antecedent for variable " ^ id ^ ") defined more than once.")
 						end
 					| _ =>