Refute: Distinguish between "genuine" and "potential" in the newly added "expect" option.

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