equal
deleted
inserted
replaced
14 |
14 |
15 open Codegen; |
15 open Codegen; |
16 |
16 |
17 val const_of = dest_Const o head_of o fst o Logic.dest_equals; |
17 val const_of = dest_Const o head_of o fst o Logic.dest_equals; |
18 |
18 |
19 structure ModuleData = TheoryDataFun |
19 structure ModuleData = Theory_Data |
20 ( |
20 ( |
21 type T = string Symtab.table; |
21 type T = string Symtab.table; |
22 val empty = Symtab.empty; |
22 val empty = Symtab.empty; |
23 val copy = I; |
|
24 val extend = I; |
23 val extend = I; |
25 fun merge _ = Symtab.merge (K true); |
24 fun merge data = Symtab.merge (K true) data; |
26 ); |
25 ); |
27 |
26 |
28 fun add_thm_target module_name thm thy = |
27 fun add_thm_target module_name thm thy = |
29 let |
28 let |
30 val (thm', _) = Code.mk_eqn thy (thm, true) |
29 val (thm', _) = Code.mk_eqn thy (thm, true) |