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