--- a/ProgTutorial/Solutions.thy	Wed Dec 02 17:08:37 2009 +0100
+++ b/ProgTutorial/Solutions.thy	Thu Dec 03 14:19:13 2009 +0100
@@ -256,10 +256,7 @@
 
 val add_conv = More_Conv.bottom_conv add_simple_conv
 
-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)*}
+fun add_tac ctxt = CONVERSION (add_conv ctxt)*}
 
 text {*
   A test case for this conversion is as follows