--- a/ProgTutorial/Tactical.thy	Sun Dec 06 14:26:14 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Fri Jan 01 00:19:11 2010 +0100
@@ -1411,10 +1411,12 @@
   \footnote{\bf FIXME: show rewriting of cterms}
 
   There is one restriction you have to keep in mind when using the simplifier:
-  it can only deal with rewriting rules that are higher order pattern 
-  (see Section \ref{sec:univ} on unification). If a rule is not a pattern,
-  then you have to use simprocs or conversions, which we shall describe in
-  the next section.
+  it can only deal with rewriting rules whose left-hand sides are higher order 
+  pattern (see Section \ref{sec:univ} on unification). Whether a term is a pattern
+  or not can be tested with the function @{ML_ind pattern in Pattern} from
+  the structure @{ML_struct Pattern}. If a rule is not a pattern and you want
+  to use it for rewriting, then you have to use simprocs or conversions, both 
+  of which we shall describe in the next section.
 
   When using the simplifier, the crucial information you have to provide is
   the simpset. If this information is not handled with care, then, as