equal
deleted
inserted
replaced
127 |
127 |
128 val (preferred_methss, message) = |
128 val (preferred_methss, message) = |
129 (case outcome of |
129 (case outcome of |
130 NONE => |
130 NONE => |
131 let |
131 let |
132 val _ = found_proof (); |
132 val _ = found_proof name; |
133 val preferred = |
133 val preferred = |
134 if smt_proofs then |
134 if smt_proofs then |
135 SMT_Method (if name = "verit" then SMT_Verit "default" else SMT_Z3) |
135 SMT_Method (if name = "verit" then SMT_Verit "default" else SMT_Z3) |
136 else |
136 else |
137 Metis_Method (NONE, NONE); |
137 Metis_Method (NONE, NONE); |