--- a/ProgTutorial/Tactical.thy	Sat Apr 24 22:55:50 2010 +0200
+++ b/ProgTutorial/Tactical.thy	Mon Apr 26 05:20:01 2010 +0200
@@ -365,16 +365,15 @@
 where
   "EQ_TRUE X \<equiv> (X = True)"
 
-lemma test: 
+schematic_lemma test: 
   shows "EQ_TRUE ?X"
 unfolding EQ_TRUE_def
 by (rule refl)
 
 text {*
-  Although Isabelle issues a warning message when stating goals involving 
-  meta-variables, it is possible to prove this theorem. The reason for the warning 
-  message is that the proved theorem is not @{text "EQ_TRUE ?X"}, as one might 
-  expect, but @{thm test}. We can test this with:
+  By using \isacommand{schematic\_lemma} it is possible to prove lemmas including
+  meta-variables on the user level. However, the proved theorem is not @{text "EQ_TRUE ?X"}, 
+  as one might expect, but @{thm test}. We can test this with:
 
   \begin{isabelle}
   \isacommand{thm}~@{thm [source] test}\\
@@ -391,6 +390,7 @@
 
 *}
 
+
 section {* Simple Tactics\label{sec:simpletacs} *}
 
 text {*
@@ -568,7 +568,7 @@
 \end{figure}
 *}
 
-lemma 
+schematic_lemma 
   shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
 apply(tactic {* Subgoal.FOCUS foc_tac @{context} 1 *})