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




