equal
deleted
inserted
replaced
474 val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp |
474 val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp |
475 |
475 |
476 fun add_facts global foldx facts = |
476 fun add_facts global foldx facts = |
477 foldx (fn (name0, ths) => fn accum => |
477 foldx (fn (name0, ths) => fn accum => |
478 if name0 <> "" andalso |
478 if name0 <> "" andalso |
479 (Long_Name.is_hidden (Facts.intern facts name0) orelse |
479 (is_some (Long_Name.dest_hidden (Facts.intern facts name0)) orelse |
480 ((Facts.is_concealed facts name0 orelse |
480 ((Facts.is_concealed facts name0 orelse |
481 (not generous andalso is_blacklisted_or_something name0)) andalso |
481 (not generous andalso is_blacklisted_or_something name0)) andalso |
482 forall (not o member Thm.eq_thm_prop add_ths) ths)) then |
482 forall (not o member Thm.eq_thm_prop add_ths) ths)) then |
483 accum |
483 accum |
484 else |
484 else |