1.1 --- a/src/HOL/Nitpick_Examples/Special_Nits.thy Thu Dec 17 15:22:27 2009 +0100
1.2 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Fri Dec 18 12:00:29 2009 +0100
1.3 @@ -135,7 +135,7 @@
1.4 lemma "\<forall>a. g a = a
1.5 \<Longrightarrow> \<exists>b\<^isub>1 b\<^isub>2 b\<^isub>3 b\<^isub>4 b\<^isub>5 b\<^isub>6 b\<^isub>7 b\<^isub>8 b\<^isub>9 b\<^isub>10 (b\<^isub>11\<Colon>nat).
1.6 b\<^isub>1 < b\<^isub>11 \<and> f5 g x = f5 (\<lambda>a. if b\<^isub>1 < b\<^isub>11 then a else h b\<^isub>2) x"
1.7 -nitpick [expect = none]
1.8 +nitpick [expect = potential]
1.9 nitpick [dont_specialize, expect = none]
1.10 nitpick [dont_box, expect = none]
1.11 nitpick [dont_box, dont_specialize, expect = none]