# HG changeset patch
# User blanchet
# Date 1236441940 -3600
# Node ID d9ecd70b111298ad81b54a18074c865a8d5465c1
# Parent  110826d1e5ffc6b7eadafa0056defb7756b0dd08
Removed "nitpick_maybe" constant. Makarius now taught me a much nicer trick.

diff -r 110826d1e5ff -r d9ecd70b1112 src/HOL/HOL.thy
--- 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
 (