1.1 --- a/src/Pure/variable.ML	Wed Feb 15 22:44:31 2012 +0100
     1.2 +++ b/src/Pure/variable.ML	Wed Feb 15 23:19:30 2012 +0100
     1.3 @@ -539,7 +539,7 @@
     1.4    in (((xs ~~ ps), t'), ctxt') end;
     1.5  
     1.6  fun forall_elim_prop t prop =
     1.7 -  Thm.beta_conversion false (Thm.capply (Thm.dest_arg prop) t)
     1.8 +  Thm.beta_conversion false (Thm.apply (Thm.dest_arg prop) t)
     1.9    |> Thm.cprop_of |> Thm.dest_arg;
    1.10  
    1.11  fun focus_cterm goal ctxt =