diff -r ff2bf50505ab -r ed2c3830d881 src/HOL/Nitpick_Examples/Induct_Nits.thy --- a/src/HOL/Nitpick_Examples/Induct_Nits.thy Tue Mar 09 09:25:23 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy Tue Mar 09 14:18:21 2010 +0100 @@ -61,7 +61,7 @@ lemma "q2 = {}" nitpick [expect = genuine] nitpick [dont_star_linear_preds, expect = genuine] -nitpick [wf, expect = likely_genuine] +nitpick [wf, expect = quasi_genuine] oops lemma "p2 = UNIV" @@ -72,7 +72,7 @@ lemma "q2 = UNIV" nitpick [expect = none] nitpick [dont_star_linear_preds, expect = none] -nitpick [wf, expect = likely_genuine] +nitpick [wf, expect = quasi_genuine] sorry lemma "p2 = q2"