# HG changeset patch
# User wenzelm
# Date 1394879287 -3600
# Node ID 39f7b7690de6d57988b622e91fce5220cdf29555
# Parent  c2c6d560e7b219a3ae5801a68fd4b4e50b19f7cd
clarified local facts;

diff -r c2c6d560e7b2 -r 39f7b7690de6 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Sat Mar 15 11:22:25 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Sat Mar 15 11:28:07 2014 +0100
@@ -386,7 +386,7 @@
     val global_facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt);
   in
     maps Facts.selections
-     (Facts.dest_static false [] local_facts @  (* FIXME exclude global_facts *)
+     (Facts.dest_static false [global_facts] local_facts @
       Facts.dest_static false [] global_facts)
   end;