144 fun define_projections fixes mutual fsum lthy = |
144 fun define_projections fixes mutual fsum lthy = |
145 let |
145 let |
146 fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = |
146 fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = |
147 let |
147 let |
148 val ((f, (_, f_defthm)), lthy') = |
148 val ((f, (_, f_defthm)), lthy') = |
149 LocalTheory.define Thm.internalK |
149 LocalTheory.define "" |
150 ((Binding.name fname, mixfix), |
150 ((Binding.name fname, mixfix), |
151 ((Binding.conceal (Binding.name (fname ^ "_def")), []), |
151 ((Binding.conceal (Binding.name (fname ^ "_def")), []), |
152 Term.subst_bound (fsum, f_def))) lthy |
152 Term.subst_bound (fsum, f_def))) lthy |
153 in |
153 in |
154 (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def, |
154 (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def, |