--- a/ProgTutorial/Tactical.thy	Tue Jul 28 12:11:33 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Thu Jul 30 11:38:52 2009 +0200
@@ -538,15 +538,19 @@
 \begin{minipage}{\textwidth}
 \begin{isabelle}
 *}
+
+
 ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = 
 let 
-  val string_of_params = string_of_cterms context params
+  val string_of_params = string_of_cterms context (map snd params)
+  val test = commas (map fst params)
   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 _ = (writeln ("params: " ^ string_of_params);
+           writeln ("param names: " ^ test);
            writeln ("schematics: " ^ string_of_schms);
            writeln ("assumptions: " ^ string_of_asms);
            writeln ("conclusion: " ^ string_of_concl);
@@ -563,7 +567,6 @@
 \end{figure}
 *}
 
-
 lemma shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
 apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
 
@@ -1056,6 +1059,8 @@
   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"}.