equal
deleted
inserted
replaced
212 options: Proof.context -> string list, |
212 options: Proof.context -> string list, |
213 reconstruct: Proof.context -> string list * SMT_Translate.recon -> |
213 reconstruct: Proof.context -> string list * SMT_Translate.recon -> |
214 int list * thm, |
214 int list * thm, |
215 default_max_relevant: int } |
215 default_max_relevant: int } |
216 |
216 |
217 fun gen_solver_head ctxt iwthms = |
217 fun gen_solver_head ctxt iwthms = SMT_Normalize.normalize iwthms ctxt |
218 SMT_Normalize.normalize ctxt iwthms |
|
219 |> rpair ctxt |
|
220 |-> SMT_Monomorph.monomorph |
|
221 |
218 |
222 fun gen_solver_tail (name, info : solver_info) rm (iwthms', ctxt) iwthms = |
219 fun gen_solver_tail (name, info : solver_info) rm (iwthms', ctxt) iwthms = |
223 let |
220 let |
224 val {env_var, is_remote, options, reconstruct, ...} = info |
221 val {env_var, is_remote, options, reconstruct, ...} = info |
225 val cmd = (rm, env_var, is_remote, name) |
222 val cmd = (rm, env_var, is_remote, name) |