changeset 51998 | f732a674db1b |
parent 51879 | ee9562d31778 |
child 52031 | 9a9238342963 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed May 15 17:27:24 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed May 15 17:43:42 2013 +0200 @@ -91,7 +91,7 @@ print silent (fn () => case outcome of - SOME failure => string_for_failure failure + SOME failure => string_of_failure failure | NONE => "Found proof" ^ (if length used_facts = length facts then ""