Can we get rid of chained state from seed_of_or2and_edge?

[yutakang]

Can we get rid of chained states from seed_of_or2and_edge?

Instead of passing a chained state that we obtain after applying certain proof methods, I would like to reconstruct such proof state by applying the methods.

PSL/Abduction/Seed_Of_Or2And_Edge.ML

Line 44 in d59677e

state : Proof.state};

[yutakang]

I need this change because the current implementation is breaking proofs here.

PSL/Abduction/Top_Down_Util.ML

Line 221 in d59677e

fun assume_cnjctrs_in_pst (name_term_pairs: (string * term) list) (pst:Proof.state): Proof.state =

I should be able to reconstruct proof using https://github.com/data61/PSL/blob/d59677eaa34db88b728ae85114d913151df1c266/PSL/Subtool.ML#L88.

PSL/PSL/Subtool.ML

Line 88 in d59677e

fun tool_output_n_timeout_to_logtac (sh_output:string) (to:real) (state:Proof.state) =