# HG changeset patch
# User blanchet
# Date 1260358002 -3600
# Node ID b174d384293e9b77855a815b8cf7c022fb512be2
# Parent  6782e3a9169f16fcd7fbe50003de8f585972ca68# Parent  bd7075c56fff2452805eb3854fd8ad444a80da3c
merged

diff -r 6782e3a9169f -r b174d384293e doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Wed Dec 09 12:07:44 2009 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Wed Dec 09 12:26:42 2009 +0100
@@ -1517,15 +1517,13 @@
 \hbox{}\qquad Free variables: \nopagebreak \\
 \hbox{}\qquad\qquad $t = N~a_3~1~\Lambda~\Lambda$ \\
 \hbox{}\qquad\qquad $x = a_4$ \\[2\smallskipamount]
-Hint: Maybe you forgot a type constraint?
 \postw
 
-It's hard to see why this is a counterexample. The hint is of no help here. To
-improve readability, we will restrict the theorem to \textit{nat}, so that we
-don't need to look up the value of the $\textit{op}~{<}$ constant to find out
-which element is smaller than the other. In addition, we will tell Nitpick to
-display the value of $\textit{insort}~t~x$ using the \textit{eval} option. This
-gives
+It's hard to see why this is a counterexample. To improve readability, we will
+restrict the theorem to \textit{nat}, so that we don't need to look up the value
+of the $\textit{op}~{<}$ constant to find out which element is smaller than the
+other. In addition, we will tell Nitpick to display the value of
+$\textit{insort}~t~x$ using the \textit{eval} option. This gives
 
 \prew
 \textbf{theorem} \textit{wf\_insort\_nat}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~(x\Colon\textit{nat}))$'' \\
diff -r 6782e3a9169f -r b174d384293e src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Dec 09 12:07:44 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Dec 09 12:26:42 2009 +0100
@@ -164,17 +164,15 @@
 (* ('a * bool option) list -> bool *)
 fun none_true asgns = forall (not_equal (SOME true) o snd) asgns
 
-val weaselly_sorts =
-  [@{sort default}, @{sort zero}, @{sort one}, @{sort plus}, @{sort minus},
-   @{sort uminus}, @{sort times}, @{sort inverse}, @{sort abs}, @{sort sgn},
-   @{sort ord}, @{sort eq}, @{sort number}]
-(* theory -> typ -> bool *)
-fun is_tfree_with_weaselly_sort thy (TFree (_, S)) =
-    exists (curry (Sign.subsort thy) S) weaselly_sorts
-  | is_tfree_with_weaselly_sort _ _ = false
-(* theory term -> bool *)
-val has_weaselly_sorts =
-  exists_type o exists_subtype o is_tfree_with_weaselly_sort
+val syntactic_sorts =
+  @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,eq}"} @
+  @{sort number}
+(* typ -> bool *)
+fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) =
+    subset (op =) (S, syntactic_sorts)
+  | has_tfree_syntactic_sort _ = false
+(* term -> bool *)
+val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort)
 
 (* (unit -> string) -> Pretty.T *)
 fun plazy f = Pretty.blk (0, pstrs (f ()))
@@ -184,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,
@@ -575,7 +581,7 @@
               | NONE => print "No confirmation by \"auto\".")
            else
              ();
-           if has_weaselly_sorts thy orig_t then
+           if has_syntactic_sorts orig_t then
              print "Hint: Maybe you forgot a type constraint?"
            else
              ();
@@ -801,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 6782e3a9169f -r b174d384293e src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Wed Dec 09 12:07:44 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Wed Dec 09 12:26:42 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 =