TFL/usyntax.ML
changeset 18176 ae9bd644d106
parent 16853 33b886cbdc8f
child 19046 bc5c6c9b114e
     1.1 --- a/TFL/usyntax.ML	Wed Nov 16 15:29:23 2005 +0100
     1.2 +++ b/TFL/usyntax.ML	Wed Nov 16 17:45:22 2005 +0100
     1.3 @@ -228,7 +228,7 @@
     1.4    | dest_term(Const(s,ty))   = CONST{Name = s, Ty = ty}
     1.5    | dest_term(M$N)           = COMB{Rator=M,Rand=N}
     1.6    | dest_term(Abs(s,ty,M))   = let  val v = Free(s,ty)
     1.7 -                               in LAMB{Bvar = v, Body = betapply (M,v)}
     1.8 +                               in LAMB{Bvar = v, Body = Term.betapply (M,v)}
     1.9                                 end
    1.10    | dest_term(Bound _)       = raise USYN_ERR "dest_term" "Bound";
    1.11  
    1.12 @@ -242,7 +242,7 @@
    1.13       let
    1.14         val s' = variant used s;
    1.15         val v = Free(s', ty);
    1.16 -     in ({Bvar = v, Body = betapply (a,v)}, s'::used)
    1.17 +     in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used)
    1.18       end
    1.19    | dest_abs _ _ =  raise USYN_ERR "dest_abs" "not an abstraction";
    1.20