# HG changeset patch
# User blanchet
# Date 1236425246 -3600
# Node ID 5598523c482ac83e6ac2ce28866445b2b1a5398b
# Parent  e9971af27b110cfd9059202b6bf190fbd7237198# Parent  91f73b2997f947fbdb8c5de9cd49276b02a0dd42
merged

diff -r e9971af27b11 -r 5598523c482a src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Sat Mar 07 10:06:58 2009 +0100
+++ b/src/HOL/Tools/refute.ML	Sat Mar 07 12:27:26 2009 +0100
@@ -1227,7 +1227,7 @@
           SatSolver.SATISFIABLE assignment =>
           (Output.priority ("*** Model found: ***\n" ^ print_model thy model
             (fn i => case assignment i of SOME b => b | NONE => true));
-           "genuine")
+           if maybe_spurious then "potential" else "genuine")
         | SatSolver.UNSATISFIABLE _ =>
           (Output.priority "No model exists.";
           case next_universe universe sizes minsize maxsize of