added a hint when the user obviously just forgot a colon after the lemma's name

--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Dec 07 11:56:01 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Dec 07 11:56:01 2010 +0100
@@ -179,6 +179,10 @@
 
 fun none_true assigns = forall (not_equal (SOME true) o snd) assigns
 
+fun has_lonely_bool_var (@{const Pure.conjunction}
+                         $ (@{const Trueprop} $ Free _) $ _) = true
+  | has_lonely_bool_var _ = false
+
 val syntactic_sorts =
   @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @
   @{sort number}
@@ -661,7 +665,9 @@
                     \section for details (\"isabelle doc nitpick\")."
             else
               ();
-            if has_syntactic_sorts orig_t then
+            if has_lonely_bool_var orig_t then
+              print "Hint: Maybe you forgot a colon after the lemma's name?"
+            else if has_syntactic_sorts orig_t then
               print "Hint: Maybe you forgot a type constraint?"
             else
               ();