changeset 53586 | bd5fa6425993 |
parent 52632 | 23393c31c7fe |
child 53761 | 4d34e267fba9 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Sep 12 20:54:26 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Sep 12 22:10:57 2013 +0200 @@ -97,7 +97,7 @@ print silent (fn () => case outcome of - SOME failure => string_of_failure failure + SOME failure => string_of_atp_failure failure | NONE => "Found proof" ^ (if length used_facts = length facts then ""