equal
deleted
inserted
replaced
14 structure RecfunCodegen : RECFUN_CODEGEN = |
14 structure RecfunCodegen : RECFUN_CODEGEN = |
15 struct |
15 struct |
16 |
16 |
17 open Codegen; |
17 open Codegen; |
18 |
18 |
19 structure CodegenArgs = |
19 structure CodegenData = TheoryDataFun |
20 struct |
20 (struct |
21 val name = "HOL/recfun_codegen"; |
21 val name = "HOL/recfun_codegen"; |
22 type T = thm list Symtab.table; |
22 type T = thm list Symtab.table; |
23 val empty = Symtab.empty; |
23 val empty = Symtab.empty; |
24 val copy = I; |
24 val copy = I; |
25 val prep_ext = I; |
25 val extend = I; |
26 val merge = Symtab.merge_multi' Drule.eq_thm_prop; |
26 fun merge _ = Symtab.merge_multi' Drule.eq_thm_prop; |
27 fun print _ _ = (); |
27 fun print _ _ = (); |
28 end; |
28 end); |
29 |
29 |
30 structure CodegenData = TheoryDataFun(CodegenArgs); |
|
31 |
30 |
32 val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop; |
31 val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop; |
33 val lhs_of = fst o dest_eqn o prop_of; |
32 val lhs_of = fst o dest_eqn o prop_of; |
34 val const_of = dest_Const o head_of o fst o dest_eqn; |
33 val const_of = dest_Const o head_of o fst o dest_eqn; |
35 |
34 |