equal
deleted
inserted
replaced
380 |
380 |
381 (* filter_theorems *) |
381 (* filter_theorems *) |
382 |
382 |
383 fun all_facts_of ctxt = |
383 fun all_facts_of ctxt = |
384 let |
384 let |
385 fun visible_facts facts = |
385 val local_facts = Proof_Context.facts_of ctxt; |
386 Facts.dest_static [] facts |
386 val global_facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt); |
387 |> filter_out (Facts.is_concealed facts o #1); |
|
388 in |
387 in |
389 maps Facts.selections |
388 maps Facts.selections |
390 (visible_facts (Proof_Context.facts_of ctxt) @ |
389 (Facts.dest_static false [] local_facts @ (* FIXME exclude global_facts *) |
391 visible_facts (Global_Theory.facts_of (Proof_Context.theory_of ctxt))) |
390 Facts.dest_static false [] global_facts) |
392 end; |
391 end; |
393 |
392 |
394 fun filter_theorems ctxt theorems query = |
393 fun filter_theorems ctxt theorems query = |
395 let |
394 let |
396 val {goal = opt_goal, limit = opt_limit, rem_dups, criteria} = query; |
395 val {goal = opt_goal, limit = opt_limit, rem_dups, criteria} = query; |