changeset 56159 | 39f7b7690de6 |
parent 56158 | c2c6d560e7b2 |
child 56467 | 8d7d6f17c6a7 |
--- 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;