# HG changeset patch
# User krauss
# Date 1301237776 -7200
# Node ID 6803f2fd15c1f5d3383d6c26b1b3176e73ab4d9b
# Parent  c17508a61f49061a63091dc620c00e4433c8f74c
avoid *** in normal output, which usually marks errors in logs

diff -r c17508a61f49 -r 6803f2fd15c1 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Sat Mar 26 21:45:29 2011 +0100
+++ b/src/HOL/Tools/refute.ML	Sun Mar 27 16:56:16 2011 +0200
@@ -1136,7 +1136,7 @@
             Output.urgent_message "Invoking SAT solver...";
             (case solver fm of
               SatSolver.SATISFIABLE assignment =>
-                (Output.urgent_message ("*** Model found: ***\n" ^ print_model ctxt model
+                (Output.urgent_message ("Model found:\n" ^ print_model ctxt model
                   (fn i => case assignment i of SOME b => b | NONE => true));
                  if maybe_spurious then "potential" else "genuine")
             | SatSolver.UNSATISFIABLE _ =>