equal
deleted
inserted
replaced
658 |
658 |
659 fun proof_result immediate (tr, proof_trs) st = |
659 fun proof_result immediate (tr, proof_trs) st = |
660 let val st' = command tr st in |
660 let val st' = command tr st in |
661 if immediate orelse |
661 if immediate orelse |
662 null proof_trs orelse |
662 null proof_trs orelse |
663 OuterKeyword.is_schematic_goal (name_of tr) orelse |
663 Keyword.is_schematic_goal (name_of tr) orelse |
664 exists (OuterKeyword.is_qed_global o name_of) proof_trs orelse |
664 exists (Keyword.is_qed_global o name_of) proof_trs orelse |
665 not (can proof_of st') orelse |
665 not (can proof_of st') orelse |
666 Proof.is_relevant (proof_of st') |
666 Proof.is_relevant (proof_of st') |
667 then |
667 then |
668 let val (states, st'') = fold_map command_result proof_trs st' |
668 let val (states, st'') = fold_map command_result proof_trs st' |
669 in (Lazy.value ((tr, st') :: (proof_trs ~~ states)), st'') end |
669 in (Lazy.value ((tr, st') :: (proof_trs ~~ states)), st'') end |