equal
deleted
inserted
replaced
66 end; |
66 end; |
67 fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts; |
67 fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts; |
68 |
68 |
69 val new_thms = |
69 val new_thms = |
70 fold (add_facts o Global_Theory.facts_of) thys [] |
70 fold (add_facts o Global_Theory.facts_of) thys [] |
71 |> sort_distinct (string_ord o pairself #1); |
71 |> sort_distinct (string_ord o apply2 #1); |
72 |
72 |
73 val used = |
73 val used = |
74 Proofterm.fold_body_thms |
74 Proofterm.fold_body_thms |
75 (fn (a, _, _) => a <> "" ? Symtab.update (a, ())) |
75 (fn (a, _, _) => a <> "" ? Symtab.update (a, ())) |
76 (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms))) |
76 (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms))) |