--- a/CookBook/Tactical.thy	Wed Mar 11 01:43:28 2009 +0000
+++ b/CookBook/Tactical.thy	Wed Mar 11 13:42:03 2009 +0000
@@ -2024,12 +2024,13 @@
   and simprocs; the advantage of conversions, however, is that you never have
   to worry about non-termination.
 
+  (FIXME: explain @{ML Conv.try_conv})
+
   \begin{exercise}\label{ex:addconversion}
   Write a tactic that does the same as the simproc in exercise
   \ref{ex:addsimproc}, but is based in conversions. That means replace terms
   of the form @{term "t\<^isub>1 + t\<^isub>2"} by their result. You can make
-  the same assumptions as in \ref{ex:addsimproc}. FIXME: the current solution
-  requires some additional functions.
+  the same assumptions as in \ref{ex:addsimproc}. 
   \end{exercise}
 
   \begin{exercise}