# HG changeset patch
# User webertj
# Date 1155131331 -7200
# Node ID a0f8e89d369d4832f6b03a6f973a0ab2e8137720
# Parent  217aada4f79540ea2d6bbcd145c9495398f34ea2
tuned: string_of_list, string_of_pair

diff -r 217aada4f795 -r a0f8e89d369d src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Wed Aug 09 10:59:58 2006 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Wed Aug 09 15:48:51 2006 +0200
@@ -300,8 +300,7 @@
 	  SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => (
 		if !trace_sat then
 			tracing ("Proof trace from SAT solver:\n" ^
-				"clauses: [" ^ commas (map (fn (c, cs) =>
-					"(" ^ string_of_int c ^ ", [" ^ commas (map string_of_int cs) ^ "])") (Inttab.dest clause_table)) ^ "]\n" ^
+				"clauses: " ^ string_of_list (string_of_pair string_of_int (string_of_list string_of_int)) (Inttab.dest clause_table) ^ "\n" ^
 				"empty clause: " ^ string_of_int empty_id)
 		else ();
 		if !quick_and_dirty then