diff -r 09b8945cac07 -r 7fe1d30c1374 src/HOL/ind_syntax.ML
--- a/src/HOL/ind_syntax.ML	Wed May 27 12:22:32 1998 +0200
+++ b/src/HOL/ind_syntax.ML	Wed May 27 12:23:45 1998 +0200
@@ -31,7 +31,8 @@
 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
 fun mk_all_imp (A,P) = 
   let val T = dest_setT (fastype_of A)
-  in  all_const T $ Abs("v", T, imp $ (mk_mem (Bound 0, A)) $ (P $ Bound 0))
+  in  all_const T $ Abs("v", T, imp $ (mk_mem (Bound 0, A)) $ 
+			        betapply(P, Bound 0))
   end;
 
 (** Disjoint sum type **)