equal
deleted
inserted
replaced
142 in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end |
142 in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end |
143 |
143 |
144 exception METIS_UNPROVABLE of unit |
144 exception METIS_UNPROVABLE of unit |
145 |
145 |
146 (* Main function to start Metis proof and reconstruction *) |
146 (* Main function to start Metis proof and reconstruction *) |
147 fun FOL_SOLVE unused (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 = |
147 fun FOL_SOLVE unused type_encs lam_trans ctxt cls ths0 = |
148 let val thy = Proof_Context.theory_of ctxt |
148 let val thy = Proof_Context.theory_of ctxt |
|
149 val type_enc :: fallback_type_encs = type_encs |
149 val new_skolem = |
150 val new_skolem = |
150 Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy) |
151 Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy) |
151 val do_lams = |
152 val do_lams = |
152 (lam_trans = liftingN orelse lam_trans = lam_liftingN) |
153 (lam_trans = liftingN orelse lam_trans = lam_liftingN) |
153 ? introduce_lam_wrappers ctxt |
154 ? introduce_lam_wrappers ctxt |