src/HOL/Tools/Nitpick/nitpick.ML

 
 fun passed_deadline NONE = false
   | passed_deadline (SOME time) = Time.compare (Time.now (), time) <> LESS
 
 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}
 fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) =

                     \induction hypothesis is not general enough or may even be \
                     \wrong. See the Nitpick manual's \"Inductive Properties\" \
                     \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
               ();
             if not genuine_means_genuine then
               if no_poly_user_axioms then