--- a/ProgTutorial/Tactical.thy	Sat Aug 01 08:59:41 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Sun Aug 02 08:44:41 2009 +0200
@@ -525,8 +525,8 @@
   Often proofs on the ML-level involve elaborate operations on assumptions and 
   @{text "\<And>"}-quantified variables. To do such operations using the basic tactics 
   shown so far is very unwieldy and brittle. Some convenience and
-  safety is provided by the functions @{ML [index] FOCUS} and @{ML [index] SUBPROOF}. 
-  These tactics fix the parameters 
+  safety is provided by the functions @{ML [index] FOCUS in Subgoal} and 
+  @{ML [index] SUBPROOF}. These tactics fix the parameters 
   and bind the various components of a goal state to a record. 
   To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
   takes a record and just prints out the content of this record (using the 
@@ -547,7 +547,7 @@
   val string_of_asms = string_of_cterms context asms
   val string_of_concl = string_of_cterm context concl
   val string_of_prems = string_of_thms_no_vars context prems   
-  val string_of_schms = string_of_cterms context (snd schematics)    
+  val string_of_schms = string_of_cterms context (map fst (snd schematics))    
  
   val _ = (writeln ("params: " ^ string_of_params);
            writeln ("schematics: " ^ string_of_schms);
@@ -557,17 +557,19 @@
 in
   all_tac 
 end*}
+
 text_raw{*
 \end{isabelle}
 \end{minipage}
 \caption{A function that prints out the various parameters provided by 
- @{ML FOCUS} and @{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for
-  extracting strings from @{ML_type cterm}s and @{ML_type thm}s.\label{fig:sptac}}
+ @{ML FOCUS in Subgoal} and @{ML SUBPROOF}. It uses the functions defined 
+  in Section~\ref{sec:printing} for extracting strings from @{ML_type cterm}s 
+  and @{ML_type thm}s.\label{fig:sptac}}
 \end{figure}
 *}
 
 lemma shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
-apply(tactic {* FOCUS foc_tac @{context} 1 *})
+apply(tactic {* Subgoal.FOCUS foc_tac @{context} 1 *})
 
 txt {*
   The tactic produces the following printout:
@@ -582,6 +584,8 @@
   \end{tabular}
   \end{quote}
 
+  (FIXME: find out how nowadays the schmetics are handled)
+
   Notice in the actual output the brown colour of the variables @{term x} and 
   @{term y}. Although they are parameters in the original goal, they are fixed inside
   the subproof. By convention these fixed variables are printed in brown colour.
@@ -593,7 +597,7 @@
 *}
 
 apply(rule impI)
-apply(tactic {* FOCUS foc_tac @{context} 1 *})
+apply(tactic {* Subgoal.FOCUS foc_tac @{context} 1 *})
 
 txt {*
   then the tactic prints out: 
@@ -613,9 +617,9 @@
 text {*
   Now also @{term "B y x"} is an assumption bound to @{text asms} and @{text prems}.
 
-  The difference between @{ML SUBPROOF} and @{ML FOCUS} is that the former
+  The difference between @{ML SUBPROOF} and @{ML FOCUS in Subgoal} is that the former
   expects that the goal is solved completely, which the latter does not.  One
-  convenience of both @{ML FOCUS} and @{ML SUBPROOF} is that we can apply the
+  convenience of both @{ML FOCUS in Subgoal} and @{ML SUBPROOF} is that we can apply the
   assumptions using the usual tactics, because the parameter @{text prems}
   contains them as theorems. With this you can easily implement a tactic that
   behaves almost like @{ML atac}:
@@ -657,13 +661,14 @@
 
 text {*
   \begin{readmore}
-  The functions @{ML FOCUS} and @{ML SUBPROOF} are defined in 
+  The functions @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are defined in 
   @{ML_file "Pure/subgoal.ML"} and also described in 
   \isccite{sec:results}. 
   \end{readmore}
 
-  Similar but less powerful functions than @{ML FOCUS} are @{ML [index] SUBGOAL}
-  and @{ML [index] CSUBGOAL}. They allow you to inspect a given subgoal (the former
+  Similar but less powerful functions than @{ML FOCUS in Subgoal} are 
+  @{ML [index] SUBGOAL} and @{ML [index] CSUBGOAL}. They allow you to 
+  inspect a given subgoal (the former
   presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type
   cterm}). With this you can implement a tactic that applies a rule according
   to the topmost logic connective in the subgoal (to illustrate this we only
@@ -1053,12 +1058,11 @@
   will solve all trivial subgoals involving @{term True} or @{term "False"}.
 
   (FIXME: say something about @{ML [index] COND} and COND')
-
-  (FIXME: say something about @{ML [index] FOCUS})
   
   \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}
 
 *}