392 val decls = map mk_decl specs; |
392 val decls = map mk_decl specs; |
393 val thy = Cont_Consts.add_consts decls thy; |
393 val thy = Cont_Consts.add_consts decls thy; |
394 fun mk_const (b, T, mx) = Const (Sign.full_name thy b, T); |
394 fun mk_const (b, T, mx) = Const (Sign.full_name thy b, T); |
395 val consts = map mk_const decls; |
395 val consts = map mk_const decls; |
396 fun mk_def c (b, t, mx) = |
396 fun mk_def c (b, t, mx) = |
397 (Binding.suffix_name "_def" b, Logic.mk_equals (c, t)); |
397 (Thm.def_binding b, Logic.mk_equals (c, t)); |
398 val defs = map2 mk_def consts specs; |
398 val defs = map2 mk_def consts specs; |
399 val (def_thms, thy) = |
399 val (def_thms, thy) = |
400 Global_Theory.add_defs false (map Thm.no_attributes defs) thy; |
400 Global_Theory.add_defs false (map Thm.no_attributes defs) thy; |
401 in |
401 in |
402 ((consts, def_thms), thy) |
402 ((consts, def_thms), thy) |