--- a/CookBook/Solutions.thy	Wed Mar 11 01:43:28 2009 +0000
+++ b/CookBook/Solutions.thy	Wed Mar 11 13:42:03 2009 +0000
@@ -95,21 +95,18 @@
 
 text {* \solution{ex:addconversion} *}
 
-text {*
-  (FIXME This solution works but is awkward.)
-*}
+ML{*fun add_simple_conv ctxt ctrm =
+let
+  val trm =  Thm.term_of ctrm
+in 
+  get_sum_thm ctxt trm (dest_sum trm)
+end
 
-ML{*fun add_conv ctxt ctrm =
+fun add_conv ctxt ctrm =
   (case Thm.term_of ctrm of
      @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => 
-         (let
-            val eq1 = Conv.binop_conv (add_conv ctxt) ctrm;
-            val ctrm' = Thm.rhs_of eq1;
-            val trm' = Thm.term_of ctrm';
-            val eq2 = Conv.rewr_conv (get_sum_thm ctxt trm' (dest_sum trm')) ctrm'
-          in
-             Thm.transitive eq1 eq2
-          end)       
+         (Conv.binop_conv (add_conv ctxt)
+          then_conv (Conv.try_conv (add_simple_conv ctxt))) ctrm         
     | _ $ _ => Conv.combination_conv 
                  (add_conv ctxt) (add_conv ctxt) ctrm
     | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm