equal
deleted
inserted
replaced
30 val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop; |
30 val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop; |
31 val lhs_of = fst o dest_eqn o prop_of; |
31 val lhs_of = fst o dest_eqn o prop_of; |
32 val const_of = dest_Const o head_of o fst o dest_eqn; |
32 val const_of = dest_Const o head_of o fst o dest_eqn; |
33 |
33 |
34 fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^ |
34 fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^ |
35 string_of_thm thm); |
35 Display.string_of_thm thm); |
36 |
36 |
37 fun add_thm opt_module thm = |
37 fun add_thm opt_module thm = |
38 (if Pattern.pattern (lhs_of thm) then |
38 (if Pattern.pattern (lhs_of thm) then |
39 RecCodegenData.map |
39 RecCodegenData.map |
40 (Symtab.cons_list ((fst o const_of o prop_of) thm, (thm, opt_module))) |
40 (Symtab.cons_list ((fst o const_of o prop_of) thm, (thm, opt_module))) |