186 (* Time.time -> Proof.state -> params -> bool -> term -> string * Proof.state *) |
186 (* Time.time -> Proof.state -> params -> bool -> term -> string * Proof.state *) |
187 fun pick_them_nits_in_term deadline state (params : params) auto orig_assm_ts |
187 fun pick_them_nits_in_term deadline state (params : params) auto orig_assm_ts |
188 orig_t = |
188 orig_t = |
189 let |
189 let |
190 val timer = Timer.startRealTimer () |
190 val timer = Timer.startRealTimer () |
191 val user_thy = Proof.theory_of state |
191 val thy = Proof.theory_of state |
|
192 val ctxt = Proof.context_of state |
192 val nitpick_thy = ThyInfo.get_theory "Nitpick" |
193 val nitpick_thy = ThyInfo.get_theory "Nitpick" |
193 val nitpick_thy_missing = not (Theory.subthy (nitpick_thy, user_thy)) |
194 val _ = Theory.subthy (nitpick_thy, thy) |
194 val thy = if nitpick_thy_missing then |
195 orelse error "You must import the theory \"Nitpick\" to use Nitpick" |
195 Theory.begin_theory "Nitpick_Internal_Name_Do_Not_Use_XYZZY" |
|
196 [nitpick_thy, user_thy] |
|
197 |> Theory.checkpoint |
|
198 else |
|
199 user_thy |
|
200 val ctxt = Proof.context_of state |
|
201 |> nitpick_thy_missing ? Context.raw_transfer thy |
|
202 val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths, |
196 val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths, |
203 boxes, monos, wfs, sat_solver, blocking, falsify, debug, verbose, |
197 boxes, monos, wfs, sat_solver, blocking, falsify, debug, verbose, |
204 overlord, user_axioms, assms, merge_type_vars, binary_ints, |
198 overlord, user_axioms, assms, merge_type_vars, binary_ints, |
205 destroy_constrs, specialize, skolemize, star_linear_preds, uncurry, |
199 destroy_constrs, specialize, skolemize, star_linear_preds, uncurry, |
206 fast_descrs, peephole_optim, tac_timeout, sym_break, sharing_depth, |
200 fast_descrs, peephole_optim, tac_timeout, sym_break, sharing_depth, |