ProgTutorial/Solutions.thy
changeset 402 a64f91de2eab
parent 391 ae2f0b40c840
child 405 f8d020bbc2c0
--- a/ProgTutorial/Solutions.thy	Sun Nov 22 15:27:10 2009 +0100
+++ b/ProgTutorial/Solutions.thy	Tue Nov 24 16:34:39 2009 +0100
@@ -254,8 +254,7 @@
      @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => 
          (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
+    | _ $ _ => Conv.comb_conv (add_conv ctxt) ctrm
     | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm
     | _ => Conv.all_conv ctrm)