--- 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 "\<forall>x. x = ?x"
+schematic_lemma "\<forall>x. x = ?x"
nitpick [expect = genuine]
oops
-lemma "\<exists>x. x = ?x"
+schematic_lemma "\<exists>x. x = ?x"
nitpick [expect = none]
by auto
-lemma "\<exists>x\<Colon>'a \<Rightarrow> 'b. x = ?x"
+schematic_lemma "\<exists>x\<Colon>'a \<Rightarrow> 'b. x = ?x"
nitpick [expect = none]
by auto
-lemma "\<forall>x. ?x = ?y"
+schematic_lemma "\<forall>x. ?x = ?y"
nitpick [expect = none]
by auto
-lemma "\<exists>x. ?x = ?y"
+schematic_lemma "\<exists>x. ?x = ?y"
nitpick [expect = none]
by auto