equal
deleted
inserted
replaced
59 [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th] |
59 [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th] |
60 in names end |
60 in names end |
61 |
61 |
62 fun all_facts_of_theory thy = |
62 fun all_facts_of_theory thy = |
63 let val ctxt = Proof_Context.init_global thy in |
63 let val ctxt = Proof_Context.init_global thy in |
64 Sledgehammer_Filter.all_facts ctxt false Symtab.empty true [] [] |
64 Sledgehammer_Fact.all_facts ctxt false Symtab.empty true [] [] |
65 (Sledgehammer_Filter.clasimpset_rule_table_of ctxt) |
65 (Sledgehammer_Fact.clasimpset_rule_table_of ctxt) |
66 |> rev (* try to restore the original order of facts, for MaSh *) |
66 |> rev (* try to restore the original order of facts, for MaSh *) |
67 end |
67 end |
68 |
68 |
69 fun inference_term [] = NONE |
69 fun inference_term [] = NONE |
70 | inference_term ss = |
70 | inference_term ss = |