# HG changeset patch
# User blanchet
# Date 1314223236 -7200
# Node ID 0989d8deab6918dde8406c065510123dfee4a1c8
# Parent  f24b990136ccc615458d869c511623feb03b1cac
include chained facts for minimizer, otherwise it won't work

diff -r f24b990136cc -r 0989d8deab69 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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;