equal
deleted
inserted
replaced
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 Abstract Syntax functions for Inductive Definitions |
6 Abstract Syntax functions for Inductive Definitions |
7 *) |
7 *) |
8 |
8 |
9 |
|
10 (*SHOULD BE ABLE TO DELETE THESE!*) |
|
11 fun flatten_typ sign T = |
|
12 let val {syn,...} = Sign.rep_sg sign |
|
13 in Pretty.str_of (Syntax.pretty_typ syn T) |
|
14 end; |
|
15 |
9 |
16 (*Make a definition, lhs==rhs, checking that vars on lhs contain *) |
10 (*Make a definition, lhs==rhs, checking that vars on lhs contain *) |
17 fun mk_defpair sign (lhs, rhs) = |
11 fun mk_defpair sign (lhs, rhs) = |
18 let val Const(name, _) = head_of lhs |
12 let val Const(name, _) = head_of lhs |
19 val dummy = assert (term_vars rhs subset term_vars lhs |
13 val dummy = assert (term_vars rhs subset term_vars lhs |