--- a/ProgTutorial/Tactical.thy	Sat Nov 12 11:45:39 2011 +0000
+++ b/ProgTutorial/Tactical.thy	Thu Nov 24 19:54:01 2011 +0000
@@ -1406,12 +1406,11 @@
   \begin{isabelle}
   \begin{tabular}{l@ {\hspace{10mm}}l}
   @{ML_ind addsimps in Raw_Simplifier}    & @{ML_ind delsimps in Raw_Simplifier}\\
-  @{ML_ind addcongs in Raw_Simplifier}    & @{ML_ind delcongs in Raw_Simplifier}\\
   @{ML_ind addsimprocs in Raw_Simplifier} & @{ML_ind delsimprocs in Raw_Simplifier}\\
+  @{ML_ind add_cong in Raw_Simplifier}    & @{ML_ind del_cong in Raw_Simplifier}\\
   \end{tabular}
   \end{isabelle}
 
-  \footnote{\bf FIXME: What about splitters? @{ML addsplits}, @{ML delsplits}}
 *}
 
 text_raw {*
@@ -1476,7 +1475,7 @@
   Adding also the congruence rule @{thm [source] UN_cong} 
 *}
 
-ML{*val ss2 = ss1 addcongs [@{thm UN_cong} RS @{thm eq_reflection}] *}
+ML{*val ss2 = Simplifier.add_cong (@{thm UN_cong} RS @{thm eq_reflection}) ss1 *}
 
 text {*
   gives