# HG changeset patch
# User blanchet
# Date 1263485195 -3600
# Node ID cb011ba389501161ca6608bbfe5a3834f2a59290
# Parent  cf9e3426c7b1a43441c77a0664541069cfb2791b
removed the Nitpick code that loaded the "Nitpick" theory explicitly if it's not already loaded, because this didn't work properly and is of doubtful value

diff -r cf9e3426c7b1 -r cb011ba38950 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Jan 14 15:06:38 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Jan 14 17:06:35 2010 +0100
@@ -188,17 +188,11 @@
                            orig_t =
   let
     val timer = Timer.startRealTimer ()
-    val user_thy = Proof.theory_of state
+    val thy = Proof.theory_of state
+    val ctxt = Proof.context_of state
     val nitpick_thy = ThyInfo.get_theory "Nitpick"
-    val nitpick_thy_missing = not (Theory.subthy (nitpick_thy, user_thy))
-    val thy = if nitpick_thy_missing then
-                Theory.begin_theory "Nitpick_Internal_Name_Do_Not_Use_XYZZY"
-                                    [nitpick_thy, user_thy]
-                |> Theory.checkpoint
-              else
-                user_thy
-    val ctxt = Proof.context_of state
-               |> nitpick_thy_missing ? Context.raw_transfer thy
+    val _ = Theory.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, monos, wfs, sat_solver, blocking, falsify, debug, verbose,
          overlord, user_axioms, assms, merge_type_vars, binary_ints,