diff -r 231ec0c45bff -r f223f8223d4a ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Wed Feb 15 14:52:03 2012 +0000
+++ b/ProgTutorial/Tactical.thy	Sun Feb 19 01:33:47 2012 +0000
@@ -2101,7 +2101,7 @@
   val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
   val two = @{cterm \"2::nat\"}
   val ten = @{cterm \"10::nat\"}
-  val ctrm = Thm.capply (Thm.capply add two) ten
+  val ctrm = Thm.apply (Thm.apply add two) ten
 in
   Thm.beta_conversion true ctrm
 end"
@@ -2119,7 +2119,7 @@
   val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
   val two = @{cterm \"2::nat\"}
   val ten = @{cterm \"10::nat\"}
-  val ctrm = Thm.capply (Thm.capply add two) ten
+  val ctrm = Thm.apply (Thm.apply add two) ten
 in
   Thm.prop_of (Thm.beta_conversion true ctrm)
 end"
@@ -2134,7 +2134,7 @@
    val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
    val two = @{cterm \"2::nat\"}
    val ten = @{cterm \"10::nat\"}
-   val ctrm = Thm.capply (Thm.capply add two) ten
+   val ctrm = Thm.apply (Thm.apply add two) ten
    val ctxt = @{context}
      |> Config.put eta_contract false 
      |> Config.put show_abbrevs false 
@@ -2187,7 +2187,7 @@
 "let
   val conv1 = Thm.beta_conversion false
   val conv2 = Conv.rewr_conv @{thm true_conj1}
-  val ctrm = Thm.capply @{cterm \"\<lambda>x. x \<and> False\"} @{cterm \"True\"}
+  val ctrm = Thm.apply @{cterm \"\<lambda>x. x \<and> False\"} @{cterm \"True\"}
 in
   (conv1 then_conv conv2) ctrm
 end"