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 Thm.internalK |
150 ((Binding.name fname, mixfix), |
150 ((Binding.name fname, mixfix), |
151 (apfst Binding.conceal Attrib.empty_binding, Term.subst_bound (fsum, f_def))) lthy |
151 ((Binding.conceal (Binding.name (fname ^ "_def")), []), |
|
152 Term.subst_bound (fsum, f_def))) lthy |
152 in |
153 in |
153 (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, |
154 f=SOME f, f_defthm=SOME f_defthm }, |
155 f=SOME f, f_defthm=SOME f_defthm }, |
155 lthy') |
156 lthy') |
156 end |
157 end |