129 fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = |
129 fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = |
130 let |
130 let |
131 val ((f, (_, f_defthm)), lthy') = |
131 val ((f, (_, f_defthm)), lthy') = |
132 Local_Theory.define |
132 Local_Theory.define |
133 ((Binding.name fname, mixfix), |
133 ((Binding.name fname, mixfix), |
134 ((Binding.conceal (Binding.name (Thm.def_name fname)), []), |
134 ((Binding.concealed (Binding.name (Thm.def_name fname)), []), |
135 Term.subst_bound (fsum, f_def))) lthy |
135 Term.subst_bound (fsum, f_def))) lthy |
136 in |
136 in |
137 (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def, |
137 (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def, |
138 f=SOME f, f_defthm=SOME f_defthm }, |
138 f=SOME f, f_defthm=SOME f_defthm }, |
139 lthy') |
139 lthy') |