Term.betapply;
authorwenzelm
Wed Nov 16 17:45:22 2005 +0100 (2005-11-16)
changeset 18176ae9bd644d106
parent 18175 7858b777569a
child 18177 7041d038acb0
Term.betapply;
TFL/tfl.ML
TFL/usyntax.ML
src/HOL/simpdata.ML
src/Sequents/Sequents.thy
src/ZF/ind_syntax.ML
     1.1 --- a/TFL/tfl.ML	Wed Nov 16 15:29:23 2005 +0100
     1.2 +++ b/TFL/tfl.ML	Wed Nov 16 17:45:22 2005 +0100
     1.3 @@ -624,7 +624,7 @@
     1.4                         "TFL fault [alpha_ex_unroll]: no correspondence"
     1.5        fun build ex      []   = []
     1.6          | build (_$rex) (v::rst) =
     1.7 -           let val ex1 = betapply(rex, v)
     1.8 +           let val ex1 = Term.betapply(rex, v)
     1.9             in  ex1 :: build ex1 rst
    1.10             end
    1.11       val (nex::exl) = rev (tm::build tm args)
    1.12 @@ -856,7 +856,7 @@
    1.13      val Rassums_TCl' = map (build_ih fconst (P,SV)) pat_TCs_list
    1.14      val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
    1.15      val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums))
    1.16 -    val cases = map (fn pat => betapply (Sinduct_assumf, pat)) pats
    1.17 +    val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
    1.18      val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
    1.19      val proved_cases = map (prove_case fconst thy) tasks
    1.20      val v = Free (variant (foldr add_term_names [] (map concl proved_cases))
     2.1 --- a/TFL/usyntax.ML	Wed Nov 16 15:29:23 2005 +0100
     2.2 +++ b/TFL/usyntax.ML	Wed Nov 16 17:45:22 2005 +0100
     2.3 @@ -228,7 +228,7 @@
     2.4    | dest_term(Const(s,ty))   = CONST{Name = s, Ty = ty}
     2.5    | dest_term(M$N)           = COMB{Rator=M,Rand=N}
     2.6    | dest_term(Abs(s,ty,M))   = let  val v = Free(s,ty)
     2.7 -                               in LAMB{Bvar = v, Body = betapply (M,v)}
     2.8 +                               in LAMB{Bvar = v, Body = Term.betapply (M,v)}
     2.9                                 end
    2.10    | dest_term(Bound _)       = raise USYN_ERR "dest_term" "Bound";
    2.11  
    2.12 @@ -242,7 +242,7 @@
    2.13       let
    2.14         val s' = variant used s;
    2.15         val v = Free(s', ty);
    2.16 -     in ({Bvar = v, Body = betapply (a,v)}, s'::used)
    2.17 +     in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used)
    2.18       end
    2.19    | dest_abs _ _ =  raise USYN_ERR "dest_abs" "not an abstraction";
    2.20  
     3.1 --- a/src/HOL/simpdata.ML	Wed Nov 16 15:29:23 2005 +0100
     3.2 +++ b/src/HOL/simpdata.ML	Wed Nov 16 17:45:22 2005 +0100
     3.3 @@ -204,7 +204,7 @@
     3.4                    let
     3.5                      val rl = cterm_instantiate [(f_Let_unfold,cf)] Let_unfold;
     3.6                    in SOME (rl OF [fx_g]) end 
     3.7 -               else if betapply (f,x) aconv g then NONE (* avoid identity conversion *)
     3.8 +               else if Term.betapply (f,x) aconv g then NONE (*avoid identity conversion*)
     3.9                 else let 
    3.10                       val abs_g'= Abs (n,xT,g');
    3.11                       val g'x = abs_g'$x;
     4.1 --- a/src/Sequents/Sequents.thy	Wed Nov 16 15:29:23 2005 +0100
     4.2 +++ b/src/Sequents/Sequents.thy	Wed Nov 16 17:45:22 2005 +0100
     4.3 @@ -90,7 +90,7 @@
     4.4        (Const("SeqO",dummyT) $ f) $
     4.5        (seqcont_tr' s) |
     4.6  (*    seqcont_tr' ((a as Abs(_,_,_)) $ s)=
     4.7 -      seqcont_tr'(betapply(a,s)) | *)
     4.8 +      seqcont_tr'(Term.betapply(a,s)) | *)
     4.9      seqcont_tr' (i $ s) =
    4.10        Const("SeqContApp",dummyT) $
    4.11        (Const("SeqId",dummyT) $ i) $
    4.12 @@ -103,7 +103,7 @@
    4.13                Const("SeqApp",dummyT) $
    4.14                (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) |
    4.15  (*            seq_itr' ((a as Abs(_,_,_)) $ s) =
    4.16 -              seq_itr'(betapply(a,s)) |    *)
    4.17 +              seq_itr'(Term.betapply(a,s)) |    *)
    4.18              seq_itr' (i $ s) =
    4.19                Const("SeqApp",dummyT) $
    4.20                (Const("SeqId",dummyT) $ i) $
     5.1 --- a/src/ZF/ind_syntax.ML	Wed Nov 16 15:29:23 2005 +0100
     5.2 +++ b/src/ZF/ind_syntax.ML	Wed Nov 16 17:45:22 2005 +0100
     5.3 @@ -30,7 +30,7 @@
     5.4  fun mk_all_imp (A,P) = 
     5.5      FOLogic.all_const iT $ 
     5.6        Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $ 
     5.7 -	           betapply(P, Bound 0));
     5.8 +	           Term.betapply(P, Bound 0));
     5.9  
    5.10  val Part_const = Const("Part", [iT,iT-->iT]--->iT);
    5.11