# HG changeset patch
# User paulson
# Date 896264625 -7200
# Node ID 7fe1d30c13740c6ccc85dbac2e3da0d8760faacf
# Parent  09b8945cac07ade9749bd1aeed5401c5d85ab2a4
mk_all_imp: no longer creates goals that have beta-redexes

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 **)
diff -r 09b8945cac07 -r 7fe1d30c1374 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Wed May 27 12:22:32 1998 +0200
+++ b/src/ZF/ind_syntax.ML	Wed May 27 12:23:45 1998 +0200
@@ -24,7 +24,8 @@
 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
 fun mk_all_imp (A,P) = 
     FOLogic.all_const iT $ 
-      Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $ (P $ Bound 0));
+      Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $ 
+	           betapply(P, Bound 0));
 
 val Part_const = Const("Part", [iT,iT-->iT]--->iT);