# HG changeset patch
# User blanchet
# Date 1282916223 -7200
# Node ID f42f425edf24243ec2d913cd875706265c9929cd
# Parent  4ec3cbd95f25a8bd265cb5a5477985c47bf6fdb3
drop chained facts

diff -r 4ec3cbd95f25 -r f42f425edf24 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Aug 27 13:27:02 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Aug 27 15:37:03 2010 +0200
@@ -357,15 +357,16 @@
     case result of
       SH_OK (time_isa, time_atp, names) =>
         let
-          fun get_thms (name, loc) =
-            ((name, loc), thms_of_name (Proof.context_of st) name)
+          fun get_thms (name, Sledgehammer_Fact_Filter.Chained) = NONE
+            | get_thms (name, loc) =
+              SOME ((name, loc), thms_of_name (Proof.context_of st) name)
         in
           change_data id inc_sh_success;
           change_data id (inc_sh_lemmas (length names));
           change_data id (inc_sh_max_lems (length names));
           change_data id (inc_sh_time_isa time_isa);
           change_data id (inc_sh_time_atp time_atp);
-          named_thms := SOME (map get_thms names);
+          named_thms := SOME (map_filter get_thms names);
           log (sh_tag id ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
             string_of_int time_atp ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
         end