src/Pure/Thy/thm_deps.ML
changeset 26699 6c7e4d858bae
parent 26697 3b9eede40608
child 27865 27a8ad9612a3
equal deleted inserted replaced
26698:ca558202ffa5 26699:6c7e4d858bae
    81 fun unused_thms (base_thys, thys) =
    81 fun unused_thms (base_thys, thys) =
    82   let
    82   let
    83     fun add_fact (name, ths) =
    83     fun add_fact (name, ths) =
    84       if exists (fn thy => PureThy.defined_fact thy name) base_thys then I
    84       if exists (fn thy => PureThy.defined_fact thy name) base_thys then I
    85       else fold_rev (fn th => (case Thm.get_name th of "" => I | a => cons (a, th))) ths;
    85       else fold_rev (fn th => (case Thm.get_name th of "" => I | a => cons (a, th))) ths;
    86     val thms = sort_wrt #1 (fold (Facts.fold_static add_fact o PureThy.facts_of) thys []);
    86     val thms =
       
    87       fold (Facts.fold_static add_fact o PureThy.facts_of) thys []
       
    88       |> sort_distinct (string_ord o pairself #1);
    87     val tab = fold Proofterm.thms_of_proof
    89     val tab = fold Proofterm.thms_of_proof
    88       (map (Proofterm.strip_thm o Thm.proof_of o snd) thms) Symtab.empty;
    90       (map (Proofterm.strip_thm o Thm.proof_of o snd) thms) Symtab.empty;
    89     fun is_unused (name, th) = case Symtab.lookup tab name of
    91     fun is_unused (name, th) = case Symtab.lookup tab name of
    90         NONE => true
    92         NONE => true
    91       | SOME ps => not (member (op aconv) (map fst ps) (Thm.prop_of th));
    93       | SOME ps => not (member (op aconv) (map fst ps) (Thm.prop_of th));