# 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;