# HG changeset patch
# User wenzelm
# Date 1601370951 -7200
# Node ID da2cbe54e53e9a8921624015b81431ef12fee0a1
# Parent  4750ea34603e6ee7ff14d48b6522c22965fdd2e0
obsolete --- ML module Nitpick resides within theory Nitpick (see also 7b8c366e34a2, 1fba360b5443);

diff -r 4750ea34603e -r da2cbe54e53e 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,