34 {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, inhabited: thm, |
34 {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, inhabited: thm, |
35 type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, |
35 type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, |
36 Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, |
36 Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, |
37 Rep_induct: thm, Abs_induct: thm}; |
37 Rep_induct: thm, Abs_induct: thm}; |
38 |
38 |
39 structure TypedefData = TheoryDataFun |
39 structure TypedefData = Theory_Data |
40 ( |
40 ( |
41 type T = info Symtab.table; |
41 type T = info Symtab.table; |
42 val empty = Symtab.empty; |
42 val empty = Symtab.empty; |
43 val copy = I; |
|
44 val extend = I; |
43 val extend = I; |
45 fun merge _ tabs : T = Symtab.merge (K true) tabs; |
44 fun merge data = Symtab.merge (K true) data; |
46 ); |
45 ); |
47 |
46 |
48 val get_info = Symtab.lookup o TypedefData.get; |
47 val get_info = Symtab.lookup o TypedefData.get; |
49 fun put_info name info = TypedefData.map (Symtab.update (name, info)); |
48 fun put_info name info = TypedefData.map (Symtab.update (name, info)); |
50 |
49 |