diff -r 9cf3bc448210 -r be6538c7b41d ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Sun Oct 25 15:26:03 2009 +0100
+++ b/ProgTutorial/General.thy	Sun Oct 25 16:12:05 2009 +0100
@@ -1093,7 +1093,7 @@
   "?P \<Longrightarrow> ?P"}
 
   This function takes first a context and second a list of strings. This list
-  specifies which variables should be turned into meta-variables once the term
+  specifies which variables should be turned into schematic variables once the term
   is proved.  The fourth argument is the term to be proved. The fifth is a
   corresponding proof given in form of a tactic (we explain tactics in
   Chapter~\ref{chp:tactical}). In the code above, the tactic proves the theorem