obsolete --- ML module Nitpick resides within theory Nitpick (see also 7b8c366e34a2, 1fba360b5443);
authorwenzelm
Tue, 29 Sep 2020 11:15:51 +0200
changeset 72327 da2cbe54e53e
parent 72326 4750ea34603e
child 72328 7cb0c5fbe2d9
obsolete --- ML module Nitpick resides within theory Nitpick (see also 7b8c366e34a2, 1fba360b5443);
src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Sep 29 09:36:14 2020 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Sep 29 11:15:51 2020 +0200
@@ -212,12 +212,6 @@
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
     val keywords = Thy_Header.get_keywords thy
-(* FIXME: reintroduce code before new release:
-
-    val nitpick_thy = Thy_Info.get_theory "Nitpick"
-    val _ = Context.subthy (nitpick_thy, thy) orelse
-            error "You must import the theory \"Nitpick\" to use Nitpick"
-*)
     val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
          boxes, finitizes, monos, wfs, sat_solver, falsify, debug, verbose,
          overlord, spy, user_axioms, assms, whacks, merge_type_vars,