# HG changeset patch
# User blanchet
# Date 1236425216 -3600
# Node ID 91f73b2997f947fbdb8c5de9cd49276b02a0dd42
# Parent  379d6f06cdb2ec78b1d22129e2363dc8cf9e3a98
Refute: Distinguish between "genuine" and "potential" in the newly added "expect" option.

diff -r 379d6f06cdb2 -r 91f73b2997f9 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Fri Mar 06 19:38:03 2009 +0100
+++ b/src/HOL/Tools/refute.ML	Sat Mar 07 12:26:56 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