equal
deleted
inserted
replaced
1 (* Title: Pure/Syntax/type_ext.ML |
1 (* Title: Pure/Syntax/type_ext.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow and Markus Wenzel, TU Muenchen |
3 Author: Tobias Nipkow and Markus Wenzel, TU Muenchen |
4 |
4 |
5 The concrete syntax of types (used to bootstrap Pure). |
5 The concrete syntax of types (used to bootstrap Pure). |
6 |
|
7 TODO: |
|
8 term_of_typ: prune sorts |
|
9 *) |
6 *) |
10 |
7 |
11 signature TYPE_EXT0 = |
8 signature TYPE_EXT0 = |
12 sig |
9 sig |
13 val raw_term_sorts: term -> (indexname * sort) list |
10 val raw_term_sorts: term -> (indexname * sort) list |