Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified local facts;
authorwenzelm
Sat, 15 Mar 2014 11:28:07 +0100
changeset 56159 39f7b7690de6
parent 56158 c2c6d560e7b2
child 56160 d348378ddf47
clarified local facts;
src/Pure/Tools/find_theorems.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle