--- a/ProgTutorial/Solutions.thy	Wed Nov 25 21:00:31 2009 +0100
+++ b/ProgTutorial/Solutions.thy	Tue Dec 01 12:25:34 2009 +0100
@@ -225,7 +225,7 @@
  
 text {* and a test case is the lemma *}
 
-lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"
+lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) ((4 + 1)::nat)"
   apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]) 1 *})
 txt {* 
   where the simproc produces the goal state
@@ -242,33 +242,28 @@
   exercise.
 *}
 
-ML{*fun add_simple_conv ctxt ctrm =
+ML {*fun add_simple_conv ctxt ctrm =
 let
-  val trm =  Thm.term_of ctrm
-in 
-  get_sum_thm ctxt trm (dest_sum trm)
+  val trm = Thm.term_of ctrm
+in
+  case trm of
+     @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => 
+        get_sum_thm ctxt trm (dest_sum trm)
+    | _ => Conv.all_conv ctrm
 end
 
-fun add_conv ctxt ctrm =
-  (case Thm.term_of ctrm of
-     @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => 
-         (Conv.binop_conv (add_conv ctxt)
-          then_conv (Conv.try_conv (add_simple_conv ctxt))) ctrm         
-    | _ $ _ => Conv.comb_conv (add_conv ctxt) ctrm
-    | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm
-    | _ => Conv.all_conv ctrm)
+val add_conv = More_Conv.bottom_conv add_simple_conv
 
-fun add_tac ctxt = CSUBGOAL (fn (goal, i) =>
-  CONVERSION
+fun add_tac ctxt = CONVERSION
     (Conv.params_conv ~1 (fn ctxt =>
        (Conv.prems_conv ~1 (add_conv ctxt) then_conv
-          Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i)*}
+          Conv.concl_conv ~1 (add_conv ctxt))) ctxt)*}
 
 text {*
   A test case for this conversion is as follows
 *}
 
-lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"
+lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) ((4 + 1)::nat)"
   apply(tactic {* add_tac @{context} 1 *})?
 txt {* 
   where it produces the goal state