equal
deleted
inserted
replaced
442 |
442 |
443 fun valid_facts facts = |
443 fun valid_facts facts = |
444 (facts, []) |-> Facts.fold_static (fn (name, ths0) => |
444 (facts, []) |-> Facts.fold_static (fn (name, ths0) => |
445 if Facts.is_concealed facts name orelse |
445 if Facts.is_concealed facts name orelse |
446 (respect_no_atp andalso is_package_def name) orelse |
446 (respect_no_atp andalso is_package_def name) orelse |
447 member (op =) multi_base_blacklist (Long_Name.base_name name) then |
447 member (op =) multi_base_blacklist (Long_Name.base_name name) orelse |
|
448 String.isSuffix "_def_raw" (* FIXME: crude hack *) name then |
448 I |
449 I |
449 else |
450 else |
450 let |
451 let |
451 fun check_thms a = |
452 fun check_thms a = |
452 (case try (ProofContext.get_thms ctxt) a of |
453 (case try (ProofContext.get_thms ctxt) a of |