diff -r 7858b777569a -r ae9bd644d106 TFL/usyntax.ML
--- 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";