# HG changeset patch
# User blanchet
# Date 1260293888 -3600
# Node ID 1fba360b54439576f09384392973d3a6e8ecbf8e
# Parent  a2736debeabdd4990beba04bd77da3632e46b4e5
made Nitpick work also for people who import "Plain" instead of "Main"

diff -r a2736debeabd -r 1fba360b5443 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 07 13:40:45 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Dec 08 18:38:08 2009 +0100
@@ -182,8 +182,16 @@
                            orig_t =
   let
     val timer = Timer.startRealTimer ()
-    val thy = Proof.theory_of state
+    val user_thy = Proof.theory_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" [nitpick_thy, user_thy]
+                |> Theory.checkpoint
+              else
+                user_thy
     val ctxt = Proof.context_of state
+               |> nitpick_thy_missing ? Context.raw_transfer thy
     val {cards_assigns, maxes_assigns, iters_assigns, bisim_depths, boxes,
          monos, wfs, sat_solver, blocking, falsify, debug, verbose, overlord,
          user_axioms, assms, merge_type_vars, destroy_constrs, specialize,
@@ -799,7 +807,7 @@
     (* int -> int -> scope list -> int * int * int -> Kodkod.outcome *)
     fun run_batches _ _ [] (max_potential, max_genuine, donno) =
         if donno > 0 andalso max_genuine > 0 then
-          (print_m (fn () => excipit "ran into difficulties"); "unknown")
+          (print_m (fn () => excipit "ran out of juice"); "unknown")
         else if max_genuine = original_max_genuine then
           if max_potential = original_max_potential then
             (print_m (K ("Nitpick found no " ^ word_model ^ ".")); "none")
diff -r a2736debeabd -r 1fba360b5443 src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Dec 07 13:40:45 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Dec 08 18:38:08 2009 +0100
@@ -250,8 +250,8 @@
 val nat_subscript = subscript o signed_string_of_int
 
 (* Time.time option -> ('a -> 'b) -> 'a -> 'b *)
-fun time_limit NONE f = f
-  | time_limit (SOME delay) f = TimeLimit.timeLimit delay f
+fun time_limit NONE = I
+  | time_limit (SOME delay) = TimeLimit.timeLimit delay
 
 (* Time.time option -> tactic -> tactic *)
 fun DETERM_TIMEOUT delay tac st =