1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Wed Feb 15 22:44:31 2012 +0100
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Wed Feb 15 23:19:30 2012 +0100
     1.3 @@ -124,8 +124,8 @@
     1.4        | _ $ _ =>
     1.5          let val (ct1, ct2) = Thm.dest_comb ct
     1.6          in 
     1.7 -          map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @
     1.8 -          map (apfst (Thm.capply ct1)) (find_vars ct2)
     1.9 +          map (apfst (fn ct => Thm.apply ct ct2)) (find_vars ct1) @
    1.10 +          map (apfst (Thm.apply ct1)) (find_vars ct2)
    1.11          end
    1.12        | _ => []);
    1.13      val eqs = maps
    1.14 @@ -136,8 +136,8 @@
    1.15            Thm.implies_elim
    1.16             (Conv.fconv_rule (Thm.beta_conversion true)
    1.17               (Drule.instantiate'
    1.18 -               [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
    1.19 -                 SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
    1.20 +               [SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct),
    1.21 +                 SOME (Thm.lambda cv' (rhs_of th)), NONE, SOME cv']
    1.22                 @{thm Suc_if_eq})) (Thm.forall_intr cv' th)
    1.23        in
    1.24          case map_filter (fn th'' =>