equal
deleted
inserted
replaced
13 |
13 |
14 structure Export_Theory: EXPORT_THEORY = |
14 structure Export_Theory: EXPORT_THEORY = |
15 struct |
15 struct |
16 |
16 |
17 (* other name spaces *) |
17 (* other name spaces *) |
18 |
|
19 fun err_dup_kind kind = error ("Duplicate name space kind " ^ quote kind); |
|
20 |
18 |
21 structure Data = Theory_Data |
19 structure Data = Theory_Data |
22 ( |
20 ( |
23 type T = (theory -> Name_Space.T) Inttab.table; |
21 type T = (theory -> Name_Space.T) Inttab.table; |
24 val empty = Inttab.empty; |
22 val empty = Inttab.empty; |