equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 signature UNPARSE_ISAC = |
6 signature UNPARSE_ISAC = |
7 sig |
7 sig |
8 eqtype term_as_string |
8 eqtype term_as_string |
9 type subst = (term * term) list |
|
10 |
9 |
11 val term_empty: term |
10 val term_empty: term |
12 val typ_empty: typ |
11 val typ_empty: typ |
13 |
12 |
14 val term: term -> term_as_string |
13 val term: term -> term_as_string |
36 structure UnparseC(**): UNPARSE_ISAC(**) = |
35 structure UnparseC(**): UNPARSE_ISAC(**) = |
37 struct |
36 struct |
38 (**) |
37 (**) |
39 |
38 |
40 type term_as_string = string; |
39 type term_as_string = string; |
41 type subst = (term * term) list; |
|
42 |
40 |
43 fun term_in_ctxt ctxt t = |
41 fun term_in_ctxt ctxt t = |
44 let |
42 let |
45 val ctxt' = Config.put show_markup false ctxt; |
43 val ctxt' = Config.put show_markup false ctxt; |
46 in |
44 in |