diff -r 3567d0571932 -r 8feb2c4bef1a src/HOL/Nitpick_Examples/Core_Nits.thy --- a/src/HOL/Nitpick_Examples/Core_Nits.thy Fri Apr 23 23:33:48 2010 +0200 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Fri Apr 23 23:35:43 2010 +0200 @@ -325,27 +325,27 @@ subsection {* Schematic Variables *} -lemma "x = ?x" +schematic_lemma "x = ?x" nitpick [expect = none] by auto -lemma "\x. x = ?x" +schematic_lemma "\x. x = ?x" nitpick [expect = genuine] oops -lemma "\x. x = ?x" +schematic_lemma "\x. x = ?x" nitpick [expect = none] by auto -lemma "\x\'a \ 'b. x = ?x" +schematic_lemma "\x\'a \ 'b. x = ?x" nitpick [expect = none] by auto -lemma "\x. ?x = ?y" +schematic_lemma "\x. ?x = ?y" nitpick [expect = none] by auto -lemma "\x. ?x = ?y" +schematic_lemma "\x. ?x = ?y" nitpick [expect = none] by auto