
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"




