equal
deleted
inserted
replaced
132 |> #1 |
132 |> #1 |
133 val atp_problem = |
133 val atp_problem = |
134 atp_problem |
134 atp_problem |
135 |> map (apsnd (filter_out (is_problem_line_tautology ctxt format))) |
135 |> map (apsnd (filter_out (is_problem_line_tautology ctxt format))) |
136 val ths = facts |> map snd |
136 val ths = facts |> map snd |
137 val all_names = ths |> map Thm.get_name_hint |
137 val all_names = ths |> map (rpair () o Thm.get_name_hint) |> Symtab.make |
138 val infers = |
138 val infers = |
139 facts |> map (fn (_, th) => |
139 facts |> map (fn (_, th) => |
140 (fact_name_of (Thm.get_name_hint th), |
140 (fact_name_of (Thm.get_name_hint th), |
141 th |> Sledgehammer_Util.thms_in_proof (SOME all_names) |
141 th |> Sledgehammer_Util.thms_in_proof (SOME all_names) |
142 |> map fact_name_of)) |
142 |> map fact_name_of)) |