more robustness in case a theorem cannot be retrieved (which typically happens with backtick facts)
authorblanchet
Tue Mar 27 16:59:13 2012 +0300 (2012-03-27)
changeset 471542c357e2b8436
parent 47153 4d4f2721b3ef
child 47155 ade3fc826af3
more robustness in case a theorem cannot be retrieved (which typically happens with backtick facts)
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
     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;