diff -r 077c764c8d8b -r 41a802bbb7df ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Mon Jul 27 10:37:28 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Tue Jul 28 08:53:05 2009 +0200
@@ -1994,7 +1994,9 @@
   variable that is abstracted and a context). The conversion that goes under
   an application is @{ML [index] combination_conv in Conv}. It expects two
   conversions as arguments, each of which is applied to the corresponding
-  ``branch'' of the application.
+  ``branch'' of the application. An abbreviation for this conversion is the
+  function @{ML [index] comb_conv in Conv}, which applies the same conversion
+  to both branches.
 
   We can now apply all these functions in a conversion that recursively
   descends a term and applies a ``@{thm [source] true_conj1}''-conversion 
@@ -2006,8 +2008,7 @@
     @{term "op \<and>"} $ @{term True} $ _ => 
       (Conv.arg_conv (all_true1_conv ctxt) then_conv
          Conv.rewr_conv @{thm true_conj1}) ctrm
-  | _ $ _ => Conv.combination_conv 
-               (all_true1_conv ctxt) (all_true1_conv ctxt) ctrm
+  | _ $ _ => Conv.comb_conv (all_true1_conv ctxt) ctrm
   | Abs _ => Conv.abs_conv (fn (_, ctxt) => all_true1_conv ctxt) ctxt ctrm
   | _ => Conv.all_conv ctrm*}
 
@@ -2038,8 +2039,7 @@
   case Thm.term_of ctrm of
     Const (@{const_name If}, _) $ _ =>
       Conv.arg_conv (all_true1_conv ctxt) ctrm
-  | _ $ _ => Conv.combination_conv 
-                (if_true1_conv ctxt) (if_true1_conv ctxt) ctrm
+  | _ $ _ => Conv.comb_conv (if_true1_conv ctxt) ctrm
   | Abs _ => Conv.abs_conv (fn (_, ctxt) => if_true1_conv ctxt) ctxt ctrm
   | _ => Conv.all_conv ctrm *}