1198 val (goal_ctxt, (_, goal_info)) = find_goal state; |
1198 val (goal_ctxt, (_, goal_info)) = find_goal state; |
1199 val {statement as (_, kind, _, prop), using, goal, before_qed, after_qed} = goal_info; |
1199 val {statement as (_, kind, _, prop), using, goal, before_qed, after_qed} = goal_info; |
1200 |
1200 |
1201 val _ = is_relevant state andalso error "Cannot fork relevant proof"; |
1201 val _ = is_relevant state andalso error "Cannot fork relevant proof"; |
1202 |
1202 |
1203 val prop' = Logic.protect prop; |
1203 val statement' = (false, kind, [[], [prop]], prop); |
1204 val statement' = (false, kind, [[], [prop']], prop'); |
|
1205 val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal) (Goal.protect (Thm.nprems_of goal) goal); |
|
1206 val after_qed' = (fn [[th]] => map_context (set_result th), fn [[th]] => set_result th); |
1204 val after_qed' = (fn [[th]] => map_context (set_result th), fn [[th]] => set_result th); |
1207 |
|
1208 val result_ctxt = |
1205 val result_ctxt = |
1209 state |
1206 state |
1210 |> map_context reset_result |
1207 |> map_context reset_result |
1211 |> map_goal I (K (statement', using, goal', before_qed, after_qed')) I |
1208 |> map_goal I (K (statement', using, goal, before_qed, after_qed')) I |
1212 |> fork_proof; |
1209 |> fork_proof; |
1213 |
1210 |
1214 val future_thm = Future.map (the_result o snd) result_ctxt; |
1211 val future_thm = Future.map (the_result o snd) result_ctxt; |
1215 val finished_goal = Goal.future_result goal_ctxt future_thm prop'; |
1212 val finished_goal = Goal.protect 0 (Goal.future_result goal_ctxt future_thm prop); |
1216 val state' = |
1213 val state' = |
1217 state |
1214 state |
1218 |> map_goal I (K (statement, using, finished_goal, NONE, after_qed)) I; |
1215 |> map_goal I (K (statement, using, finished_goal, NONE, after_qed)) I; |
1219 in (Future.map fst result_ctxt, state') end; |
1216 in (Future.map fst result_ctxt, state') end; |
1220 |
1217 |