equal
deleted
inserted
replaced
89 |
89 |
90 fun add_defs defs ctxt = |
90 fun add_defs defs ctxt = |
91 let |
91 let |
92 val ((bvars, mxs), specs) = defs |> split_list |>> split_list; |
92 val ((bvars, mxs), specs) = defs |> split_list |>> split_list; |
93 val ((bfacts, atts), rhss) = specs |> split_list |>> split_list; |
93 val ((bfacts, atts), rhss) = specs |> split_list |>> split_list; |
94 val xs = map Name.name_of bvars; |
94 val xs = map Binding.base_name bvars; |
95 val names = map2 (Binding.map_base o Thm.def_name_optional) xs bfacts; |
95 val names = map2 (Binding.map_base o Thm.def_name_optional) xs bfacts; |
96 val eqs = mk_def ctxt (xs ~~ rhss); |
96 val eqs = mk_def ctxt (xs ~~ rhss); |
97 val lhss = map (fst o Logic.dest_equals) eqs; |
97 val lhss = map (fst o Logic.dest_equals) eqs; |
98 in |
98 in |
99 ctxt |
99 ctxt |