equal
deleted
inserted
replaced
65 | simple_ast_of (Var (xi, _)) = Variable (string_of_vname xi) |
65 | simple_ast_of (Var (xi, _)) = Variable (string_of_vname xi) |
66 | simple_ast_of (t as _ $ _) = |
66 | simple_ast_of (t as _ $ _) = |
67 let val (f, args) = strip_comb t in |
67 let val (f, args) = strip_comb t in |
68 mk_appl (simple_ast_of f) (map simple_ast_of args) |
68 mk_appl (simple_ast_of f) (map simple_ast_of args) |
69 end |
69 end |
70 | simple_ast_of (Bound _) = sys_error "simple_ast_of: Bound" |
70 | simple_ast_of (Bound i) = Variable ("B." ^ string_of_int i) |
71 | simple_ast_of (Abs _) = sys_error "simple_ast_of: Abs"; |
71 | simple_ast_of (Abs _) = sys_error "simple_ast_of: Abs"; |
72 |
72 |
73 |
73 |
74 |
74 |
75 (** typ_to_ast **) |
75 (** typ_to_ast **) |