# HG changeset patch
# User blanchet
# Date 1532117982 -7200
# Node ID c9570658e8f13cb31634a811f059fa4e0efce8d4
# Parent  96aae7c44bb2159ae0748039dc60f1531f6a71fe
don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)

diff -r 96aae7c44bb2 -r c9570658e8f1 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 10:09:59 2018 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:42 2018 +0200
@@ -424,8 +424,13 @@
                    (case isar_proof of
                      Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) =>
                      let
-                       val used_facts' = filter (fn (s, (sc, _)) =>
-                         member (op =) gfs s andalso sc <> Chained) used_facts
+                       val used_facts' =
+                         map_filter (fn s =>
+                            if exists (fn (s', (sc, _)) => s' = s andalso sc = Chained)
+                                used_facts then
+                              NONE
+                            else
+                              SOME (s, (Global, General))) gfs
                      in
                        ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count)
                      end)