--- a/ProgTutorial/Tactical.thy	Fri May 29 12:15:48 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Sat May 30 11:12:46 2009 +0200
@@ -694,7 +694,7 @@
   quantified variable. So you really have to construct the pattern using the
   basic term-constructors. This is not necessary in other cases, because their
   type is always fixed to function types involving only the type @{typ
-  bool}. (See Section \ref{sec:terms_types_manually} about constructing terms
+  bool}. (See Section \ref{sec:terms_manually} about constructing terms
   manually.) For the catch-all pattern, we chose to just return @{ML all_tac}. 
   Consequently, @{ML select_tac} never fails.