src/HOL/Tools/Nitpick/nitpick.ML
changeset 72327 da2cbe54e53e
parent 72298 a540283d6b58
child 72328 7cb0c5fbe2d9
equal deleted inserted replaced
72326:4750ea34603e 72327:da2cbe54e53e
   210     val time_start = Time.now ()
   210     val time_start = Time.now ()
   211     val timer = Timer.startRealTimer ()
   211     val timer = Timer.startRealTimer ()
   212     val thy = Proof.theory_of state
   212     val thy = Proof.theory_of state
   213     val ctxt = Proof.context_of state
   213     val ctxt = Proof.context_of state
   214     val keywords = Thy_Header.get_keywords thy
   214     val keywords = Thy_Header.get_keywords thy
   215 (* FIXME: reintroduce code before new release:
       
   216 
       
   217     val nitpick_thy = Thy_Info.get_theory "Nitpick"
       
   218     val _ = Context.subthy (nitpick_thy, thy) orelse
       
   219             error "You must import the theory \"Nitpick\" to use Nitpick"
       
   220 *)
       
   221     val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
   215     val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
   222          boxes, finitizes, monos, wfs, sat_solver, falsify, debug, verbose,
   216          boxes, finitizes, monos, wfs, sat_solver, falsify, debug, verbose,
   223          overlord, spy, user_axioms, assms, whacks, merge_type_vars,
   217          overlord, spy, user_axioms, assms, whacks, merge_type_vars,
   224          binary_ints, destroy_constrs, specialize, star_linear_preds,
   218          binary_ints, destroy_constrs, specialize, star_linear_preds,
   225          total_consts, needs, peephole_optim, datatype_sym_break,
   219          total_consts, needs, peephole_optim, datatype_sym_break,