equal
deleted
inserted
replaced
134 false true [] @{prop False} |
134 false true [] @{prop False} |
135 |> #1 |
135 |> #1 |
136 val atp_problem = |
136 val atp_problem = |
137 atp_problem |
137 atp_problem |
138 |> map (apsnd (filter_out (is_problem_line_tautology ctxt format))) |
138 |> map (apsnd (filter_out (is_problem_line_tautology ctxt format))) |
139 val ths = facts |> map snd |
139 val all_names = Sledgehammer_Fact.build_all_names Thm.get_name_hint facts |
140 val all_names = ths |> map (rpair () o Thm.get_name_hint) |> Symtab.make |
|
141 val infers = |
140 val infers = |
142 facts |> map (fn (_, th) => |
141 facts |
143 (fact_name_of (Thm.get_name_hint th), |
142 |> map (fn (_, th) => |
144 th |> Sledgehammer_Util.thms_in_proof (SOME all_names) |
143 (fact_name_of (Thm.get_name_hint th), |
145 |> map fact_name_of)) |
144 th |> Sledgehammer_Util.thms_in_proof (SOME all_names) |
|
145 |> map fact_name_of)) |
146 val all_atp_problem_names = |
146 val all_atp_problem_names = |
147 atp_problem |> maps (map ident_of_problem_line o snd) |
147 atp_problem |> maps (map ident_of_problem_line o snd) |
148 val infers = |
148 val infers = |
149 infers |> filter (member (op =) all_atp_problem_names o fst) |
149 infers |> filter (member (op =) all_atp_problem_names o fst) |
150 |> map (apsnd (filter (member (op =) all_atp_problem_names))) |
150 |> map (apsnd (filter (member (op =) all_atp_problem_names))) |