src/ZF/ind_syntax.ML
changeset 4972 7fe1d30c1374
parent 4804 02b7c759159b
child 6053 8a1059aa01f0
     1.1 --- a/src/ZF/ind_syntax.ML	Wed May 27 12:22:32 1998 +0200
     1.2 +++ b/src/ZF/ind_syntax.ML	Wed May 27 12:23:45 1998 +0200
     1.3 @@ -24,7 +24,8 @@
     1.4  (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
     1.5  fun mk_all_imp (A,P) = 
     1.6      FOLogic.all_const iT $ 
     1.7 -      Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $ (P $ Bound 0));
     1.8 +      Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $ 
     1.9 +	           betapply(P, Bound 0));
    1.10  
    1.11  val Part_const = Const("Part", [iT,iT-->iT]--->iT);
    1.12