equal
deleted
inserted
replaced
86 |> ProofContext.sticky_prefix prfx |
86 |> ProofContext.sticky_prefix prfx |
87 |> ProofContext.qualified_names |
87 |> ProofContext.qualified_names |
88 |> (snd o ProofContext.note_thmss_i "" notes) |
88 |> (snd o ProofContext.note_thmss_i "" notes) |
89 |> ProofContext.restore_naming ctxt |
89 |> ProofContext.restore_naming ctxt |
90 end) #> |
90 end) #> |
91 Proof.put_facts NONE #> Seq.single; |
91 Proof.put_facts NONE; |
92 in |
92 in |
93 state' |
93 state' |
94 |> Proof.chain_facts chain_facts |
94 |> Proof.chain_facts chain_facts |
95 |> Proof.local_goal (K (K ())) (K I) ProofContext.bind_propp_schematic_i |
95 |> Proof.local_goal (K (K ())) (K I) ProofContext.bind_propp_schematic_i |
96 "invoke" NONE after_qed propp |
96 "invoke" NONE after_qed propp |