equal
deleted
inserted
replaced
177 else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res)) |
177 else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res)) |
178 end); |
178 end); |
179 val res = |
179 val res = |
180 if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (Future.enabled ()) |
180 if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (Future.enabled ()) |
181 then result () |
181 then result () |
182 else future_result ctxt' (Future.fork_pri 1 result) (Thm.term_of stmt); |
182 else future_result ctxt' (Future.fork_pri ~1 result) (Thm.term_of stmt); |
183 in |
183 in |
184 Conjunction.elim_balanced (length props) res |
184 Conjunction.elim_balanced (length props) res |
185 |> map (Assumption.export false ctxt' ctxt) |
185 |> map (Assumption.export false ctxt' ctxt) |
186 |> Variable.export ctxt' ctxt |
186 |> Variable.export ctxt' ctxt |
187 |> map Drule.zero_var_indexes |
187 |> map Drule.zero_var_indexes |