# HG changeset patch
# User wenzelm
# Date 1165775847 -3600
# Node ID 09f62e99859ec234e904c4032e1aca9cf9e24d79
# Parent  22dd32812116d371c0537add8ff796c7fe106012
ML_Syntax.print_XXX;

diff -r 22dd32812116 -r 09f62e99859e src/HOL/Library/MLString.thy
--- a/src/HOL/Library/MLString.thy	Sun Dec 10 19:37:26 2006 +0100
+++ b/src/HOL/Library/MLString.thy	Sun Dec 10 19:37:27 2006 +0100
@@ -66,8 +66,9 @@
   (Haskell "_")
 
 setup {*
-  CodegenSerializer.add_pretty_ml_string "SML" "List.list.Nil" "List.list.Cons" "MLString.ml_string.STR"
-    HOLogic.print_char HOLogic.print_string "String.implode"
+  CodegenSerializer.add_pretty_ml_string "SML"
+    "List.list.Nil" "List.list.Cons" "MLString.ml_string.STR"
+    ML_Syntax.print_char ML_Syntax.print_string "String.implode"
 *}
 
 code_const explode
diff -r 22dd32812116 -r 09f62e99859e src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Sun Dec 10 19:37:26 2006 +0100
+++ b/src/HOL/Tools/sat_funcs.ML	Sun Dec 10 19:37:27 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: " ^ 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)) ^ ")")
+					tracing ("Resolving clause: " ^ string_of_thm c1 ^ " (hyps: " ^ ML_Syntax.print_list (Sign.string_of_term (theory_of_thm c1)) (#hyps (rep_thm c1))
+						^ ")\nwith clause: " ^ string_of_thm c2 ^ " (hyps: " ^ ML_Syntax.print_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: " ^ ML_Syntax.str_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.print_list (Sign.string_of_term (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
 				else ()
 			val _ = inc counter
 		in
@@ -334,7 +334,7 @@
 	  SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => (
 		if !trace_sat then
 			tracing ("Proof trace from SAT solver:\n" ^
-				"clauses: " ^ ML_Syntax.str_of_list (ML_Syntax.str_of_pair Int.toString (ML_Syntax.str_of_list Int.toString)) (Inttab.dest clause_table) ^ "\n" ^
+				"clauses: " ^ ML_Syntax.print_list (ML_Syntax.print_pair Int.toString (ML_Syntax.print_list Int.toString)) (Inttab.dest clause_table) ^ "\n" ^
 				"empty clause: " ^ Int.toString empty_id)
 		else ();
 		if !quick_and_dirty then