equal
deleted
inserted
replaced
5 |
5 |
6 Definitions that have to be reread after init_thy_reader has been invoked |
6 Definitions that have to be reread after init_thy_reader has been invoked |
7 *) |
7 *) |
8 |
8 |
9 fun simpset_of tname = |
9 fun simpset_of tname = |
10 case get_thydata (theory_of tname) "simpset" of |
10 case get_thydata tname "simpset" of |
11 None => empty_ss |
11 None => empty_ss |
12 | Some (SS_DATA ss) => ss; |
12 | Some (SS_DATA ss) => ss; |
13 |
13 |
14 fun datatypes_of tname = |
14 fun datatypes_of tname = |
15 case get_thydata (theory_of tname) "datatypes" of |
15 case get_thydata tname "datatypes" of |
16 None => [] |
16 None => [] |
17 | Some (DT_DATA ds) => ds; |
17 | Some (DT_DATA ds) => ds; |