equal
deleted
inserted
replaced
47 val name = Thm.def_name_optional c raw_name; |
47 val name = Thm.def_name_optional c raw_name; |
48 val atts = map (prep_att thy) raw_atts; |
48 val atts = map (prep_att thy) raw_atts; |
49 |
49 |
50 val thy' = |
50 val thy' = |
51 thy |
51 thy |
52 |> Theory.add_consts_i [(c, T, mx)] |
52 |> Sign.add_consts_i [(c, T, mx)] |
53 |> PureThy.add_defs_i false [((name, def), atts)] |
53 |> PureThy.add_defs_i false [((name, def), atts)] |
54 |-> (fn [thm] => CodegenData.add_func false thm); |
54 |-> (fn [thm] => CodegenData.add_func false thm); |
55 in ((c, T), thy') end; |
55 in ((c, T), thy') end; |
56 |
56 |
57 fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy = |
57 fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy = |