179 val timer = Timer.startRealTimer () |
179 val timer = Timer.startRealTimer () |
180 val thy = Proof.theory_of state |
180 val thy = Proof.theory_of state |
181 val ctxt = Proof.context_of state |
181 val ctxt = Proof.context_of state |
182 (* FIXME: reintroduce code before new release: |
182 (* FIXME: reintroduce code before new release: |
183 |
183 |
184 val nitpick_thy = ThyInfo.get_theory "Nitpick" |
184 val nitpick_thy = Thy_Info.get_theory "Nitpick" |
185 val _ = Theory.subthy (nitpick_thy, thy) orelse |
185 val _ = Theory.subthy (nitpick_thy, thy) orelse |
186 error "You must import the theory \"Nitpick\" to use Nitpick" |
186 error "You must import the theory \"Nitpick\" to use Nitpick" |
187 *) |
187 *) |
188 val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths, |
188 val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths, |
189 boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug, |
189 boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug, |