equal
deleted
inserted
replaced
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 |> Sign.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 false [((name, def), atts)] |
54 |-> (fn [thm] => Code.add_default_func thm); |
54 |-> (fn [thm] => Code.add_default_func 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 = |
58 let |
58 let |