diff -r 2728e8daebc0 -r 0cbd34857b9e ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Mon Aug 03 14:01:57 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Mon Aug 03 16:47:01 2009 +0200
@@ -1060,7 +1060,6 @@
   \begin{readmore}
   Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}.
   Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}.
-  The function @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are defined in @{ML_file "Pure/subgoal.ML"}
   \end{readmore}
 
 *}