equal
deleted
inserted
replaced
77 (* check for success and print out some information on failure *) |
77 (* check for success and print out some information on failure *) |
78 val failure = find_failure proof |
78 val failure = find_failure proof |
79 val success = rc = 0 andalso is_none failure |
79 val success = rc = 0 andalso is_none failure |
80 val message = |
80 val message = |
81 if success then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno) |
81 if success then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno) |
82 else "Could not prove." |
82 else "Could not prove goal." |
83 val _ = if isSome failure |
83 val _ = if isSome failure |
84 then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof) |
84 then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof) |
85 else () |
85 else () |
86 val _ = if rc <> 0 |
86 val _ = if rc <> 0 |
87 then Output.debug (fn () => "Sledgehammer exited with return code " ^ string_of_int rc ^ ":\n" ^ proof) |
87 then Output.debug (fn () => "Sledgehammer exited with return code " ^ string_of_int rc ^ ":\n" ^ proof) |