1.1 --- a/doc-src/Nitpick/nitpick.tex	Mon Dec 07 12:21:15 2009 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Mon Dec 07 13:40:45 2009 +0100
     1.3 @@ -1517,15 +1517,13 @@
     1.4  \hbox{}\qquad Free variables: \nopagebreak \\
     1.5  \hbox{}\qquad\qquad $t = N~a_3~1~\Lambda~\Lambda$ \\
     1.6  \hbox{}\qquad\qquad $x = a_4$ \\[2\smallskipamount]
     1.7 -Hint: Maybe you forgot a type constraint?
     1.8  \postw
     1.9  
    1.10 -It's hard to see why this is a counterexample. The hint is of no help here. To
    1.11 -improve readability, we will restrict the theorem to \textit{nat}, so that we
    1.12 -don't need to look up the value of the $\textit{op}~{<}$ constant to find out
    1.13 -which element is smaller than the other. In addition, we will tell Nitpick to
    1.14 -display the value of $\textit{insort}~t~x$ using the \textit{eval} option. This
    1.15 -gives
    1.16 +It's hard to see why this is a counterexample. To improve readability, we will
    1.17 +restrict the theorem to \textit{nat}, so that we don't need to look up the value
    1.18 +of the $\textit{op}~{<}$ constant to find out which element is smaller than the
    1.19 +other. In addition, we will tell Nitpick to display the value of
    1.20 +$\textit{insort}~t~x$ using the \textit{eval} option. This gives
    1.21  
    1.22  \prew
    1.23  \textbf{theorem} \textit{wf\_insort\_nat}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~(x\Colon\textit{nat}))$'' \\

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 07 12:21:15 2009 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 07 13:40:45 2009 +0100
     2.3 @@ -164,17 +164,15 @@
     2.4  (* ('a * bool option) list -> bool *)
     2.5  fun none_true asgns = forall (not_equal (SOME true) o snd) asgns
     2.6  
     2.7 -val weaselly_sorts =
     2.8 -  [@{sort default}, @{sort zero}, @{sort one}, @{sort plus}, @{sort minus},
     2.9 -   @{sort uminus}, @{sort times}, @{sort inverse}, @{sort abs}, @{sort sgn},
    2.10 -   @{sort ord}, @{sort eq}, @{sort number}]
    2.11 -(* theory -> typ -> bool *)
    2.12 -fun is_tfree_with_weaselly_sort thy (TFree (_, S)) =
    2.13 -    exists (curry (Sign.subsort thy) S) weaselly_sorts
    2.14 -  | is_tfree_with_weaselly_sort _ _ = false
    2.15 -(* theory term -> bool *)
    2.16 -val has_weaselly_sorts =
    2.17 -  exists_type o exists_subtype o is_tfree_with_weaselly_sort
    2.18 +val syntactic_sorts =
    2.19 +  @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,eq}"} @
    2.20 +  @{sort number}
    2.21 +(* typ -> bool *)
    2.22 +fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) =
    2.23 +    subset (op =) (S, syntactic_sorts)
    2.24 +  | has_tfree_syntactic_sort _ = false
    2.25 +(* term -> bool *)
    2.26 +val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort)
    2.27  
    2.28  (* (unit -> string) -> Pretty.T *)
    2.29  fun plazy f = Pretty.blk (0, pstrs (f ()))
    2.30 @@ -575,7 +573,7 @@
    2.31                | NONE => print "No confirmation by \"auto\".")
    2.32             else
    2.33               ();
    2.34 -           if has_weaselly_sorts thy orig_t then
    2.35 +           if has_syntactic_sorts orig_t then
    2.36               print "Hint: Maybe you forgot a type constraint?"
    2.37             else
    2.38               ();