# HG changeset patch
# User wenzelm
# Date 1164239511 -3600
# Node ID 936edc65a3a5223e3d095e47d4d80721418b6cd6
# Parent  02054bf31c0ef7462c69418bb3e6dd8eb9ad4a9d
renamed string_of_pair/list/option to ML_Syntax.str_of_pair/list/option;

diff -r 02054bf31c0e -r 936edc65a3a5 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Thu Nov 23 00:51:47 2006 +0100
+++ b/src/HOL/Tools/sat_funcs.ML	Thu Nov 23 00:51:51 2006 +0100
@@ -139,8 +139,8 @@
 		fun resolution (c1, hyp1_table) (c2, hyp2_table) =
 		let
 			val _ = if !trace_sat then
-					tracing ("Resolving clause: " ^ string_of_thm c1 ^ " (hyps: " ^ string_of_list (Sign.string_of_term (theory_of_thm c1)) (#hyps (rep_thm c1))
-						^ ")\nwith clause: " ^ string_of_thm c2 ^ " (hyps: " ^ string_of_list (Sign.string_of_term (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
+					tracing ("Resolving clause: " ^ string_of_thm c1 ^ " (hyps: " ^ ML_Syntax.str_of_list (Sign.string_of_term (theory_of_thm c1)) (#hyps (rep_thm c1))
+						^ ")\nwith clause: " ^ string_of_thm c2 ^ " (hyps: " ^ ML_Syntax.str_of_list (Sign.string_of_term (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
 				else ()
 
 			(* the two literals used for resolution *)
@@ -172,7 +172,7 @@
 			val hypnew_table = Inttab.merge (K true) (Inttab.delete i1 hyp1_table, Inttab.delete (~i1) hyp2_table)
 
 			val _ = if !trace_sat then
-					tracing ("Resulting clause: " ^ string_of_thm c_new ^ " (hyps: " ^ string_of_list (Sign.string_of_term (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
+					tracing ("Resulting clause: " ^ string_of_thm c_new ^ " (hyps: " ^ ML_Syntax.str_of_list (Sign.string_of_term (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
 				else ()
 			val _ = inc counter
 		in
@@ -324,7 +324,7 @@
 	  SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => (
 		if !trace_sat then
 			tracing ("Proof trace from SAT solver:\n" ^
-				"clauses: " ^ string_of_list (string_of_pair string_of_int (string_of_list string_of_int)) (Inttab.dest clause_table) ^ "\n" ^
+				"clauses: " ^ ML_Syntax.str_of_list (ML_Syntax.str_of_pair string_of_int (ML_Syntax.str_of_list string_of_int)) (Inttab.dest clause_table) ^ "\n" ^
 				"empty clause: " ^ string_of_int empty_id)
 		else ();
 		if !quick_and_dirty then