--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Aug 31 15:30:11 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Aug 31 17:32:29 2009 +0200
@@ -63,11 +63,12 @@
fun get_thms ctxt = maps (thms_of_name ctxt)
fun metis thms ctxt = MetisTools.metis_tac ctxt thms
fun apply_metis thms = "\nApplying metis with these theorems: " ^
- (if try (Mirabelle.can_apply (metis thms)) st = SOME true
+ (if Mirabelle.can_apply (metis thms) st
then "success"
else "failure")
val msg = if not (AList.defined (op =) args metisK) then ""
- else apply_metis (get_thms (Proof.context_of st) (these thm_names))
+ else (apply_metis (get_thms (Proof.context_of st) (these thm_names))
+ handle ERROR m => "\nException: " ^ m)
in
if success
then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")" ^ msg)