equal
deleted
inserted
replaced
158 val immediate_proof = local_immediate_proof o global_immediate_proof; |
158 val immediate_proof = local_immediate_proof o global_immediate_proof; |
159 val done_proof = local_done_proof o global_done_proof; |
159 val done_proof = local_done_proof o global_done_proof; |
160 val skip_proof = local_skip_proof o global_skip_proof; |
160 val skip_proof = local_skip_proof o global_skip_proof; |
161 |
161 |
162 val forget_proof = |
162 val forget_proof = |
163 Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current) o |
163 Toplevel.proof_to_theory (Sign.local_path o Sign.restore_naming ProtoPure.thy o (* FIXME tmp *) |
|
164 Proof.theory_of o ProofHistory.current) o |
164 Toplevel.skip_proof_to_theory (K true); |
165 Toplevel.skip_proof_to_theory (K true); |
165 |
166 |
166 |
167 |
167 (* theory init and exit *) |
168 (* theory init and exit *) |
168 |
169 |