diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Mon Jan 10 15:30:17 2011 +0100
+++ b/src/HOL/Tools/sat_funcs.ML	Mon Jan 10 15:45:46 2011 +0100
@@ -346,9 +346,9 @@
        (if !trace_sat then
           tracing ("Proof trace from SAT solver:\n" ^
             "clauses: " ^ ML_Syntax.print_list
-              (ML_Syntax.print_pair Int.toString (ML_Syntax.print_list Int.toString))
+              (ML_Syntax.print_pair ML_Syntax.print_int (ML_Syntax.print_list ML_Syntax.print_int))
               (Inttab.dest clause_table) ^ "\n" ^
-            "empty clause: " ^ Int.toString empty_id)
+            "empty clause: " ^ string_of_int empty_id)
         else ();
         if !quick_and_dirty then
           make_quick_and_dirty_thm ()