diff -r 3567d0571932 -r 8feb2c4bef1a src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Fri Apr 23 23:33:48 2010 +0200
+++ b/src/HOL/ex/Refute_Examples.thy	Fri Apr 23 23:35:43 2010 +0200
@@ -347,12 +347,12 @@
 
 subsubsection {* Schematic variables *}
 
-lemma "?P"
+schematic_lemma "?P"
   refute
   apply auto
 done
 
-lemma "x = ?y"
+schematic_lemma "x = ?y"
   refute
   apply auto
 done