mk_all_imp: no longer creates goals that have beta-redexes
authorpaulson
Wed May 27 12:23:45 1998 +0200 (1998-05-27 ago)
changeset 49727fe1d30c1374
parent 4971 09b8945cac07
child 4973 7420178bd2d9
mk_all_imp: no longer creates goals that have beta-redexes
src/HOL/ind_syntax.ML
src/ZF/ind_syntax.ML
     1.1 --- a/src/HOL/ind_syntax.ML	Wed May 27 12:22:32 1998 +0200
     1.2 +++ b/src/HOL/ind_syntax.ML	Wed May 27 12:23:45 1998 +0200
     1.3 @@ -31,7 +31,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    let val T = dest_setT (fastype_of A)
     1.7 -  in  all_const T $ Abs("v", T, imp $ (mk_mem (Bound 0, A)) $ (P $ Bound 0))
     1.8 +  in  all_const T $ Abs("v", T, imp $ (mk_mem (Bound 0, A)) $ 
     1.9 +			        betapply(P, Bound 0))
    1.10    end;
    1.11  
    1.12  (** Disjoint sum type **)
     2.1 --- a/src/ZF/ind_syntax.ML	Wed May 27 12:22:32 1998 +0200
     2.2 +++ b/src/ZF/ind_syntax.ML	Wed May 27 12:23:45 1998 +0200
     2.3 @@ -24,7 +24,8 @@
     2.4  (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
     2.5  fun mk_all_imp (A,P) = 
     2.6      FOLogic.all_const iT $ 
     2.7 -      Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $ (P $ Bound 0));
     2.8 +      Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $ 
     2.9 +	           betapply(P, Bound 0));
    2.10  
    2.11  val Part_const = Const("Part", [iT,iT-->iT]--->iT);
    2.12