# HG changeset patch
# User blanchet
# Date 1291719361 -3600
# Node ID d5ebe94248ad28b5c6e32914ad518cb78020909f
# Parent  9f1d3fcef1ca91aa4ca63ab297e5f89591b769aa
added a hint when the user obviously just forgot a colon after the lemma's name

diff -r 9f1d3fcef1ca -r d5ebe94248ad src/HOL/Tools/Nitpick/nitpick.ML
--- 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
               ();