# HG changeset patch
# User blanchet
# Date 1332856753 -10800
# Node ID 2c357e2b8436127c3d0dfa21de9eb8f7ba34802e
# Parent  4d4f2721b3ef22a758aea6dfd5b1faa113ca3c89
more robustness in case a theorem cannot be retrieved (which typically happens with backtick facts)

diff -r 4d4f2721b3ef -r 2c357e2b8436 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Mar 27 16:59:13 2012 +0300
@@ -520,7 +520,8 @@
       SH_OK (time_isa, time_prover, names) =>
         let
           fun get_thms (name, stature) =
-            SOME ((name, stature), thms_of_name (Proof.context_of st) name)
+            try (thms_of_name (Proof.context_of st)) name
+            |> Option.map (pair (name, stature))
         in
           change_data id inc_sh_success;
           if trivial then () else change_data id inc_sh_nontriv_success;