diff -r 000000000000 -r a5a9c433f639 src/Pure/Syntax/parse_tree.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Syntax/parse_tree.ML	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,63 @@
+(*  Title:      Pure/Syntax/parse_tree
+    ID:         $Id$
+    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
+*)
+
+signature PARSE_TREE =
+sig
+  structure Lexicon: LEXICON
+  structure Ast: AST
+  local open Lexicon Ast in
+    datatype ParseTree =
+      Node of string * ParseTree list |
+      Tip of Token
+    val mk_pt: string * ParseTree list -> ParseTree
+    val pt_to_ast: (string -> (ast list -> ast) option) -> ParseTree -> ast
+  end
+end;
+
+functor ParseTreeFun(structure Lexicon: LEXICON and Ast: AST): PARSE_TREE =
+struct
+
+structure Lexicon = Lexicon;
+structure Ast = Ast;
+open Lexicon Ast;
+
+
+(* datatype ParseTree *)  (* FIXME rename *)
+
+datatype ParseTree =
+  Node of string * ParseTree list |
+  Tip of Token;
+
+
+(* mk_pt *)
+
+fun mk_pt("", [pt]) = pt
+  | mk_pt("", _) = error "mk_pt: funny copy op in parse tree"
+  | mk_pt(s, ptl) = Node (s, ptl);
+
+
+(* pt_to_ast *)
+
+fun pt_to_ast trf pt =
+  let
+    fun trans a args =
+      (case trf a of
+        None => mk_appl (Constant a) args
+      | Some f =>
+          (f args) handle _ => error ("pt_to_ast: error in translation for " ^ a));
+
+    fun trav (Node (a, pts)) = trans a (map trav pts)
+      | trav (Tip (IdentSy x)) = Variable x
+      | trav (Tip (VarSy xi)) = Variable (string_of_vname xi)
+      | trav (Tip (TFreeSy x)) = Variable x
+      | trav (Tip (TVarSy xi)) = Variable (string_of_vname xi)
+      | trav (Tip _) = error "pt_to_ast: unexpected token in parse tree";
+  in
+    trav pt
+  end;
+
+
+end;
+