more robustness in case a theorem cannot be retrieved (which typically happens with backtick facts)

--- 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;