diff -r 8057d65607eb -r d0b81d6e1b28 ProgTutorial/Package/Ind_Code.thy
--- a/ProgTutorial/Package/Ind_Code.thy	Sat Aug 01 08:59:41 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Sun Aug 02 08:44:41 2009 +0200
@@ -598,7 +598,8 @@
   The problem with @{ML SUBPROOF}, however, is that it always expects us to 
   completely discharge the goal (see Section~\ref{sec:simpletacs}). This is 
   a bit inconvenient for our gradual explanation of the proof here. Therefore
-  we use first the function @{ML [index] FOCUS}, which does same as @{ML SUBPROOF} 
+  we use first the function @{ML [index] FOCUS in Subgoal}, which does s
+  ame as @{ML SUBPROOF} 
   but does not require us to completely discharge the goal. 
 *}
 (*<*)oops(*>*)
@@ -630,13 +631,13 @@
   First we calculate the values for @{text "params1/2"} and @{text "prems1/2"}
   from @{text "params"} and @{text "prems"}, respectively. To better see what is
   going in our example, we will print out these values using the printing
-  function in Figure~\ref{fig:chopprint}. Since @{ML FOCUS} will
+  function in Figure~\ref{fig:chopprint}. Since @{ML FOCUS in Subgoal} will
   supply us the @{text "params"} and @{text "prems"} as lists, we can 
   separate them using the function @{ML [index] chop}. 
 *}
 
 ML %linenosgray{*fun chop_test_tac preds rules =
-  FOCUS (fn {params, prems, context, ...} =>
+  Subgoal.FOCUS (fn {params, prems, context, ...} =>
   let
     val cparams = map snd params
     val (params1, params2) = chop (length cparams - length preds) cparams
@@ -704,7 +705,7 @@
 *}
 
 ML %linenosgray{*fun apply_prem_tac i preds rules =
-  FOCUS (fn {params, prems, context, ...} =>
+  Subgoal.FOCUS (fn {params, prems, context, ...} =>
   let
     val cparams = map snd params
     val (params1, params2) = chop (length cparams - length preds) cparams
@@ -788,7 +789,7 @@
   end) *}
 
 text {*
-  Note that the tactic is now @{ML SUBPROOF}, not @{ML FOCUS} anymore. 
+  Note that the tactic is now @{ML SUBPROOF}, not @{ML FOCUS in Subgoal} anymore. 
   The full proof of the introduction rule is as follows:
 *}