--- 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
--- 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