changeset 30347 | 91f73b2997f9 |
parent 30314 | 853778f6ef7d |
child 30349 | 110826d1e5ff |
--- 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