I have implemented (in SML) a parser which parses an lambda term in concrete syntax (given as a string) into an SML expression of type term. The function is parse : string -> term.

To use this parser, copy the file loadparser.sml to your working directory and then "use" it. This will define the term datatype so you should not define it yourself. Here are some examples of its use:

- parse "x y";
val it = App (Var "x",Var "y") : term

- parse "fn x => x y";
val it = Abs ("x",App (Var "x",Var "y")) : term

- parse "fn x => fn y => fn z => (x z) (y z)";
val it =
  Abs
    ("x",Abs ("y",Abs ("z",App (App (Var "x",Var "z"),App (Var "y",Var "z")))))
  : term