src/ZF/ex/misc.thy

--- a/src/ZF/ex/misc.thy	Tue Oct 06 13:31:44 2015 +0200
+++ b/src/ZF/ex/misc.thy	Tue Oct 06 15:14:28 2015 +0200
@@ -44,7 +44,7 @@
 by (blast intro!: equalityI)
 
 text\<open>trivial example of term synthesis: apparently hard for some provers!\<close>
-schematic_lemma "a \<noteq> b ==> a:?X & b \<notin> ?X"
+schematic_goal "a \<noteq> b ==> a:?X & b \<notin> ?X"
 by blast
 
 text\<open>Nice blast benchmark.  Proved in 0.3s; old tactics can't manage it!\<close>