Term.betapply;

--- a/TFL/tfl.ML	Wed Nov 16 15:29:23 2005 +0100
+++ b/TFL/tfl.ML	Wed Nov 16 17:45:22 2005 +0100
@@ -624,7 +624,7 @@
                        "TFL fault [alpha_ex_unroll]: no correspondence"
       fun build ex      []   = []
         | build (_$rex) (v::rst) =
-           let val ex1 = betapply(rex, v)
+           let val ex1 = Term.betapply(rex, v)
            in  ex1 :: build ex1 rst
            end
      val (nex::exl) = rev (tm::build tm args)
@@ -856,7 +856,7 @@
     val Rassums_TCl' = map (build_ih fconst (P,SV)) pat_TCs_list
     val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
     val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums))
-    val cases = map (fn pat => betapply (Sinduct_assumf, pat)) pats
+    val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
     val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
     val proved_cases = map (prove_case fconst thy) tasks
     val v = Free (variant (foldr add_term_names [] (map concl proved_cases))

--- a/TFL/usyntax.ML	Wed Nov 16 15:29:23 2005 +0100
+++ b/TFL/usyntax.ML	Wed Nov 16 17:45:22 2005 +0100
@@ -228,7 +228,7 @@
   | dest_term(Const(s,ty))   = CONST{Name = s, Ty = ty}
   | dest_term(M$N)           = COMB{Rator=M,Rand=N}
   | dest_term(Abs(s,ty,M))   = let  val v = Free(s,ty)
-                               in LAMB{Bvar = v, Body = betapply (M,v)}
+                               in LAMB{Bvar = v, Body = Term.betapply (M,v)}
                                end
   | dest_term(Bound _)       = raise USYN_ERR "dest_term" "Bound";
 
@@ -242,7 +242,7 @@
      let
        val s' = variant used s;
        val v = Free(s', ty);
-     in ({Bvar = v, Body = betapply (a,v)}, s'::used)
+     in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used)
      end
   | dest_abs _ _ =  raise USYN_ERR "dest_abs" "not an abstraction";
 

--- a/src/HOL/simpdata.ML	Wed Nov 16 15:29:23 2005 +0100
+++ b/src/HOL/simpdata.ML	Wed Nov 16 17:45:22 2005 +0100
@@ -204,7 +204,7 @@
                   let
                     val rl = cterm_instantiate [(f_Let_unfold,cf)] Let_unfold;
                   in SOME (rl OF [fx_g]) end 
-               else if betapply (f,x) aconv g then NONE (* avoid identity conversion *)
+               else if Term.betapply (f,x) aconv g then NONE (*avoid identity conversion*)
                else let 
                      val abs_g'= Abs (n,xT,g');
                      val g'x = abs_g'$x;

--- a/src/Sequents/Sequents.thy	Wed Nov 16 15:29:23 2005 +0100
+++ b/src/Sequents/Sequents.thy	Wed Nov 16 17:45:22 2005 +0100
@@ -90,7 +90,7 @@
       (Const("SeqO",dummyT) $ f) $
       (seqcont_tr' s) |
 (*    seqcont_tr' ((a as Abs(_,_,_)) $ s)=
-      seqcont_tr'(betapply(a,s)) | *)
+      seqcont_tr'(Term.betapply(a,s)) | *)
     seqcont_tr' (i $ s) =
       Const("SeqContApp",dummyT) $
       (Const("SeqId",dummyT) $ i) $
@@ -103,7 +103,7 @@
               Const("SeqApp",dummyT) $
               (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) |
 (*            seq_itr' ((a as Abs(_,_,_)) $ s) =
-              seq_itr'(betapply(a,s)) |    *)
+              seq_itr'(Term.betapply(a,s)) |    *)
             seq_itr' (i $ s) =
               Const("SeqApp",dummyT) $
               (Const("SeqId",dummyT) $ i) $

--- a/src/ZF/ind_syntax.ML	Wed Nov 16 15:29:23 2005 +0100
+++ b/src/ZF/ind_syntax.ML	Wed Nov 16 17:45:22 2005 +0100
@@ -30,7 +30,7 @@
 fun mk_all_imp (A,P) = 
     FOLogic.all_const iT $ 
       Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $ 
-	           betapply(P, Bound 0));
+	           Term.betapply(P, Bound 0));
 
 val Part_const = Const("Part", [iT,iT-->iT]--->iT);