--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Aug 24 22:12:30 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Aug 25 00:00:36 2011 +0200
@@ -484,9 +484,8 @@
case result of
SH_OK (time_isa, time_prover, names) =>
let
- fun get_thms (_, ATP_Translate.Chained) = NONE
- | get_thms (name, loc) =
- SOME ((name, loc), thms_of_name (Proof.context_of st) name)
+ fun get_thms (name, loc) =
+ SOME ((name, loc), thms_of_name (Proof.context_of st) name)
in
change_data id inc_sh_success;
if trivial then () else change_data id inc_sh_nontriv_success;