--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Oct 06 13:31:44 2015 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Oct 06 15:14:28 2015 +0200
@@ -266,27 +266,27 @@
subsection {* Schematic Variables *}
-schematic_lemma "x = ?x"
+schematic_goal "x = ?x"
nitpick [expect = none]
by auto
-schematic_lemma "\<forall>x. x = ?x"
+schematic_goal "\<forall>x. x = ?x"
nitpick [expect = genuine]
oops
-schematic_lemma "\<exists>x. x = ?x"
+schematic_goal "\<exists>x. x = ?x"
nitpick [expect = none]
by auto
-schematic_lemma "\<exists>x::'a \<Rightarrow> 'b. x = ?x"
+schematic_goal "\<exists>x::'a \<Rightarrow> 'b. x = ?x"
nitpick [expect = none]
by auto
-schematic_lemma "\<forall>x. ?x = ?y"
+schematic_goal "\<forall>x. ?x = ?y"
nitpick [expect = none]
by auto
-schematic_lemma "\<exists>x. ?x = ?y"
+schematic_goal "\<exists>x. ?x = ?y"
nitpick [expect = none]
by auto