# 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 ();