148 fun define_projections fixes mutual fsum lthy = |
148 fun define_projections fixes mutual fsum lthy = |
149 let |
149 let |
150 fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = |
150 fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = |
151 let |
151 let |
152 val ((f, (_, f_defthm)), lthy') = |
152 val ((f, (_, f_defthm)), lthy') = |
153 LocalTheory.define Thm.internalK ((fname, mixfix), |
153 LocalTheory.define Thm.internalK ((Name.binding fname, mixfix), |
154 ((fname ^ "_def", []), Term.subst_bound (fsum, f_def))) |
154 ((Name.binding (fname ^ "_def"), []), Term.subst_bound (fsum, f_def))) |
155 lthy |
155 lthy |
156 in |
156 in |
157 (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def, |
157 (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def, |
158 f=SOME f, f_defthm=SOME f_defthm }, |
158 f=SOME f, f_defthm=SOME f_defthm }, |
159 lthy') |
159 lthy') |