--- 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"