47 (* unused_thms *) |
47 (* unused_thms *) |
48 |
48 |
49 fun unused_thms (base_thys, thys) = |
49 fun unused_thms (base_thys, thys) = |
50 let |
50 let |
51 fun add_fact space (name, ths) = |
51 fun add_fact space (name, ths) = |
52 if exists (fn thy => PureThy.defined_fact thy name) base_thys then I |
52 if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I |
53 else |
53 else |
54 let val {concealed, group, ...} = Name_Space.the_entry space name in |
54 let val {concealed, group, ...} = Name_Space.the_entry space name in |
55 fold_rev (fn th => |
55 fold_rev (fn th => |
56 (case Thm.derivation_name th of |
56 (case Thm.derivation_name th of |
57 "" => I |
57 "" => I |
58 | a => cons (a, (th, concealed, group)))) ths |
58 | a => cons (a, (th, concealed, group)))) ths |
59 end; |
59 end; |
60 fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts; |
60 fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts; |
61 |
61 |
62 val new_thms = |
62 val new_thms = |
63 fold (add_facts o PureThy.facts_of) thys [] |
63 fold (add_facts o Global_Theory.facts_of) thys [] |
64 |> sort_distinct (string_ord o pairself #1); |
64 |> sort_distinct (string_ord o pairself #1); |
65 |
65 |
66 val used = |
66 val used = |
67 Proofterm.fold_body_thms |
67 Proofterm.fold_body_thms |
68 (fn (a, prop, _) => a <> "" ? Symtab.insert_list (op =) (a, prop)) |
68 (fn (a, prop, _) => a <> "" ? Symtab.insert_list (op =) (a, prop)) |