1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Mar 27 16:59:13 2012 +0300
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Mar 27 16:59:13 2012 +0300
     1.3 @@ -520,7 +520,8 @@
     1.4        SH_OK (time_isa, time_prover, names) =>
     1.5          let
     1.6            fun get_thms (name, stature) =
     1.7 -            SOME ((name, stature), thms_of_name (Proof.context_of st) name)
     1.8 +            try (thms_of_name (Proof.context_of st)) name
     1.9 +            |> Option.map (pair (name, stature))
    1.10          in
    1.11            change_data id inc_sh_success;
    1.12            if trivial then () else change_data id inc_sh_nontriv_success;