Removed "nitpick_maybe" constant. Makarius now taught me a much nicer trick.

--- a/src/HOL/HOL.thy	Sat Mar 07 16:47:36 2009 +0100
+++ b/src/HOL/HOL.thy	Sat Mar 07 17:05:40 2009 +0100
@@ -1710,8 +1710,6 @@
 
 text {* This will be relocated once Nitpick is moved to HOL. *}
 
-consts nitpick_maybe :: "'a \<Rightarrow> 'a" ("_\<^isub>?" [40] 40)
-
 ML {*
 structure Nitpick_Const_Def_Thms = NamedThmsFun
 (